let A be non empty set ; :: thesis: for f, g, h, f1 being Element of Funcs (A,REAL)
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 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds
f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds
g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds
h . z = 0 ) & f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds
f1 . z = 0 ) holds
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 f, g, h, f1 be Element of Funcs (A,REAL); :: 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 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds
f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds
g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds
h . z = 0 ) & f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds
f1 . z = 0 ) holds
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 & f . x1 = 1 & ( for z being set st z in A & z <> x1 holds
f . z = 0 ) & g . x2 = 1 & ( for z being set st z in A & z <> x2 holds
g . z = 0 ) & h . x3 = 1 & ( for z being set st z in A & z <> x3 holds
h . z = 0 ) & f1 . x4 = 1 & ( for z being set st z in A & z <> x4 holds
f1 . z = 0 ) implies 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 that
A1: A = {x1,x2,x3,x4} and
A2: x1 <> x2 and
A3: x1 <> x3 and
A4: x1 <> x4 and
A5: x2 <> x3 and
A6: x2 <> x4 and
A7: x3 <> x4 and
A8: f . x1 = 1 and
A9: for z being set st z in A & z <> x1 holds
f . z = 0 and
A10: g . x2 = 1 and
A11: for z being set st z in A & z <> x2 holds
g . z = 0 and
A12: h . x3 = 1 and
A13: for z being set st z in A & z <> x3 holds
h . z = 0 and
A14: f1 . x4 = 1 and
A15: for z being set st z in A & z <> x4 holds
f1 . z = 0 ; :: 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]))
A16: ( f . x4 = 0 & g . x4 = 0 ) by A4, A6, A9, A11;
A17: f1 . x3 = 0 by ;
A18: f1 . x2 = 0 by ;
A19: ( f . x2 = 0 & h . x2 = 0 ) by A2, A5, A9, A13;
A20: f1 . x1 = 0 by ;
A21: ( g . x1 = 0 & h . x1 = 0 ) by A2, A3, A11, A13;
A22: h . x4 = 0 by ;
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]))
take a = h9 . x1; :: thesis: ex b, c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))
take b = h9 . x2; :: thesis: ex c, d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))
take c = h9 . x3; :: thesis: ex d being Real st h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))
take d = h9 . x4; :: thesis: h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))
A23: ( f . x3 = 0 & g . x3 = 0 ) by A3, A5, A9, A11;
now :: thesis: for x being Element of A holds h9 . x = (() . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))) . x
let x be Element of A; :: thesis: h9 . x = (() . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))) . x
A24: ( x = x1 or x = x2 or x = x3 or x = x4 ) by ;
A25: (() . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))) . x2 = ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))) . x2) + ((() . [d,f1]) . x2) by FUNCSDOM:1
.= (((() . ((() . [a,f]),(() . [b,g]))) . x2) + ((() . [c,h]) . x2)) + ((() . [d,f1]) . x2) by FUNCSDOM:1
.= ((((() . [a,f]) . x2) + ((() . [b,g]) . x2)) + ((() . [c,h]) . x2)) + ((() . [d,f1]) . x2) by FUNCSDOM:1
.= ((((() . [a,f]) . x2) + ((() . [b,g]) . x2)) + ((() . [c,h]) . x2)) + (d * (f1 . x2)) by FUNCSDOM:4
.= ((((() . [a,f]) . x2) + ((() . [b,g]) . x2)) + (c * (h . x2))) + (d * (f1 . x2)) by FUNCSDOM:4
.= ((((() . [a,f]) . x2) + (b * (g . x2))) + (c * (h . x2))) + (d * (f1 . x2)) by FUNCSDOM:4
.= (((a * 0) + (b * 1)) + (c * 0)) + (d * 0) by
.= h9 . x2 ;
A26: (() . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))) . x4 = ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))) . x4) + ((() . [d,f1]) . x4) by FUNCSDOM:1
.= (((() . ((() . [a,f]),(() . [b,g]))) . x4) + ((() . [c,h]) . x4)) + ((() . [d,f1]) . x4) by FUNCSDOM:1
.= ((((() . [a,f]) . x4) + ((() . [b,g]) . x4)) + ((() . [c,h]) . x4)) + ((() . [d,f1]) . x4) by FUNCSDOM:1
.= ((((() . [a,f]) . x4) + ((() . [b,g]) . x4)) + ((() . [c,h]) . x4)) + (d * (f1 . x4)) by FUNCSDOM:4
.= ((((() . [a,f]) . x4) + ((() . [b,g]) . x4)) + (c * (h . x4))) + (d * (f1 . x4)) by FUNCSDOM:4
.= ((((() . [a,f]) . x4) + (b * (g . x4))) + (c * (h . x4))) + (d * (f1 . x4)) by FUNCSDOM:4
.= (((a * 0) + (b * 0)) + (c * 0)) + (d * 1) by
.= h9 . x4 ;
A27: (() . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))) . x3 = ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))) . x3) + ((() . [d,f1]) . x3) by FUNCSDOM:1
.= (((() . ((() . [a,f]),(() . [b,g]))) . x3) + ((() . [c,h]) . x3)) + ((() . [d,f1]) . x3) by FUNCSDOM:1
.= ((((() . [a,f]) . x3) + ((() . [b,g]) . x3)) + ((() . [c,h]) . x3)) + ((() . [d,f1]) . x3) by FUNCSDOM:1
.= ((((() . [a,f]) . x3) + ((() . [b,g]) . x3)) + ((() . [c,h]) . x3)) + (d * (f1 . x3)) by FUNCSDOM:4
.= ((((() . [a,f]) . x3) + ((() . [b,g]) . x3)) + (c * (h . x3))) + (d * (f1 . x3)) by FUNCSDOM:4
.= ((((() . [a,f]) . x3) + (b * (g . x3))) + (c * (h . x3))) + (d * (f1 . x3)) by FUNCSDOM:4
.= (((a * 0) + (b * 0)) + (c * 1)) + (d * 0) by
.= h9 . x3 ;
(() . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))) . x1 = ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))) . x1) + ((() . [d,f1]) . x1) by FUNCSDOM:1
.= (((() . ((() . [a,f]),(() . [b,g]))) . x1) + ((() . [c,h]) . x1)) + ((() . [d,f1]) . x1) by FUNCSDOM:1
.= ((((() . [a,f]) . x1) + ((() . [b,g]) . x1)) + ((() . [c,h]) . x1)) + ((() . [d,f1]) . x1) by FUNCSDOM:1
.= ((((() . [a,f]) . x1) + ((() . [b,g]) . x1)) + ((() . [c,h]) . x1)) + (d * (f1 . x1)) by FUNCSDOM:4
.= ((((() . [a,f]) . x1) + ((() . [b,g]) . x1)) + (c * (h . x1))) + (d * (f1 . x1)) by FUNCSDOM:4
.= ((((() . [a,f]) . x1) + (b * (g . x1))) + (c * (h . x1))) + (d * (f1 . x1)) by FUNCSDOM:4
.= (((a * 1) + (b * 0)) + (c * 0)) + (d * 0) by
.= h9 . x1 ;
hence h9 . x = (() . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1]))) . x by A24, A25, A27, A26; :: thesis: verum
end;
hence h9 = () . ((() . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h]))),(() . [d,f1])) by FUNCT_2:63; :: thesis: verum