let A be non empty set ; for f, g, h being Element of Funcs (A,REAL)
for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 & 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 ) holds
for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))
let f, g, h be Element of Funcs (A,REAL); for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 & 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 ) holds
for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))
let x1, x2, x3 be Element of A; ( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 & 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 ) implies for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) )
assume that
A1:
A = {x1,x2,x3}
and
A2:
x1 <> x2
and
A3:
x1 <> x3
and
A4:
x2 <> x3
and
A5:
f . x1 = 1
and
A6:
for z being set st z in A & z <> x1 holds
f . z = 0
and
A7:
g . x2 = 1
and
A8:
for z being set st z in A & z <> x2 holds
g . z = 0
and
A9:
h . x3 = 1
and
A10:
for z being set st z in A & z <> x3 holds
h . z = 0
; for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))
A11:
( g . x1 = 0 & h . x1 = 0 )
by A2, A3, A8, A10;
A12:
( f . x2 = 0 & h . x2 = 0 )
by A2, A4, A6, A10;
let h9 be Element of Funcs (A,REAL); ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))
take a = h9 . x1; ex b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))
take b = h9 . x2; ex c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))
take c = h9 . x3; h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))
A13:
( f . x3 = 0 & g . x3 = 0 )
by A3, A4, A6, A8;
now for x being Element of A holds h9 . x = ((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . xlet x be
Element of
A;
h9 . x = ((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . xA14:
(
x = x1 or
x = x2 or
x = x3 )
by A1, ENUMSET1:def 1;
A15:
((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x2 =
(((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x2) + (((RealFuncExtMult A) . [c,h]) . x2)
by FUNCSDOM:1
.=
((((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)) + (((RealFuncExtMult A) . [c,h]) . x2)
by FUNCSDOM:1
.=
((((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2)) + (c * (h . x2))
by FUNCSDOM:4
.=
((((RealFuncExtMult A) . [a,f]) . x2) + (b * (g . x2))) + (c * (h . x2))
by FUNCSDOM:4
.=
((a * 0) + (b * 1)) + (c * 0)
by A7, A12, FUNCSDOM:4
.=
h9 . x2
;
A16:
((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x3 =
(((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x3) + (((RealFuncExtMult A) . [c,h]) . x3)
by FUNCSDOM:1
.=
((((RealFuncExtMult A) . [a,f]) . x3) + (((RealFuncExtMult A) . [b,g]) . x3)) + (((RealFuncExtMult A) . [c,h]) . x3)
by FUNCSDOM:1
.=
((((RealFuncExtMult A) . [a,f]) . x3) + (((RealFuncExtMult A) . [b,g]) . x3)) + (c * (h . x3))
by FUNCSDOM:4
.=
((((RealFuncExtMult A) . [a,f]) . x3) + (b * (g . x3))) + (c * (h . x3))
by FUNCSDOM:4
.=
((a * 0) + (b * 0)) + (c * 1)
by A9, A13, FUNCSDOM:4
.=
h9 . x3
;
((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x1 =
(((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x1) + (((RealFuncExtMult A) . [c,h]) . x1)
by FUNCSDOM:1
.=
((((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)) + (((RealFuncExtMult A) . [c,h]) . x1)
by FUNCSDOM:1
.=
((((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1)) + (c * (h . x1))
by FUNCSDOM:4
.=
((((RealFuncExtMult A) . [a,f]) . x1) + (b * (g . x1))) + (c * (h . x1))
by FUNCSDOM:4
.=
((a * 1) + (b * 0)) + (c * 0)
by A5, A11, FUNCSDOM:4
.=
h9 . x1
;
hence
h9 . x = ((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x
by A14, A15, A16;
verum end;
hence
h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))
by FUNCT_2:63; verum