let A be non empty set ; :: thesis: for f, g, h being Element of Funcs (A,REAL)
for x1, x2, x3 being Element of A st 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 a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 )
let f, g, h be Element of Funcs (A,REAL); :: thesis: for x1, x2, x3 being Element of A st 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 a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 )
let x1, x2, x3 be Element of A; :: thesis: ( 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 a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 ) )
set RM = RealFuncExtMult A;
set RA = RealFuncAdd A;
assume that
A1: x1 <> x2 and
A2: x1 <> x3 and
A3: x2 <> x3 and
A4: f . x1 = 1 and
A5: for z being set st z in A & z <> x1 holds
f . z = 0 and
A6: g . x2 = 1 and
A7: for z being set st z in A & z <> x2 holds
g . z = 0 and
A8: h . x3 = 1 and
A9: for z being set st z in A & z <> x3 holds
h . z = 0 ; :: thesis: for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 )
A10: ( f . x2 = 0 & h . x2 = 0 ) by A1, A3, A5, A9;
let a, b, c be Real; :: thesis: ( (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A implies ( a = 0 & b = 0 & c = 0 ) )
assume A11: (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A ; :: thesis: ( a = 0 & b = 0 & c = 0 )
reconsider a = a, b = b, c = c as Element of REAL by XREAL_0:def 1;
A12: 0 = ((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x2 by FUNCOP_1:7, A11
.= (((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 A6, A10, FUNCSDOM:4
.= b ;
A13: ( g . x1 = 0 & h . x1 = 0 ) by A1, A2, A7, A9;
A14: ( f . x3 = 0 & g . x3 = 0 ) by A2, A3, A5, A7;
A15: 0 = ((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x3 by A11, FUNCOP_1:7
.= (((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 A8, A14, FUNCSDOM:4
.= c ;
0 = ((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))) . x1 by A11, FUNCOP_1:7
.= (((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 A4, A13, FUNCSDOM:4
.= a ;
hence ( a = 0 & b = 0 & c = 0 ) by A12, A15; :: thesis: verum