let A be non empty set ; :: thesis: for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
ex f, g, h, f1 being Element of Funcs (A,REAL) st
for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))

let x1, x2, x3, x4 be Element of A; :: thesis: ( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies ex f, g, h, f1 being Element of Funcs (A,REAL) st
for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1])) )

assume A1: ( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 ) ; :: thesis: ex f, g, h, f1 being Element of Funcs (A,REAL) st
for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))

consider f being Element of Funcs (A,REAL) such that
A2: ( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds
f . z = 0 ) ) by Th10;
consider f1 being Element of Funcs (A,REAL) such that
A3: ( f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds
f1 . z = 0 ) ) by Th10;
consider h being Element of Funcs (A,REAL) such that
A4: ( h . x3 = 1 & ( for z being set st z in A & z <> x3 holds
h . z = 0 ) ) by Th10;
consider g being Element of Funcs (A,REAL) such that
A5: ( g . x2 = 1 & ( for z being set st z in A & z <> x2 holds
g . z = 0 ) ) by Th10;
take f ; :: thesis: ex g, h, f1 being Element of Funcs (A,REAL) st
for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))

take g ; :: thesis: ex h, f1 being Element of Funcs (A,REAL) st
for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))

take h ; :: thesis: ex f1 being Element of Funcs (A,REAL) st
for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))

take f1 ; :: thesis: for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))
let h9 be Element of Funcs (A,REAL); :: thesis: ex a, b, c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))
thus ex a, b, c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1])) by A1, A2, A5, A4, A3, Th19; :: thesis: verum