let x1, x2 be set ; :: thesis: for A being non empty set
for f, g being Element of Funcs A,REAL st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) holds
for a, b being Real st (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]) = RealFuncZero A holds
( a = 0 & b = 0 )
let A be non empty set ; :: thesis: for f, g being Element of Funcs A,REAL st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) holds
for a, b being Real st (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]) = RealFuncZero A holds
( a = 0 & b = 0 )
let f, g be Element of Funcs A,REAL ; :: thesis: ( x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) implies for a, b being Real st (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]) = RealFuncZero A holds
( a = 0 & b = 0 ) )
assume that
A1: x1 in A and
A2: x2 in A and
A3: x1 <> x2 and
A4: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1 ) ) ) ) ; :: thesis: for a, b being Real st (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]) = RealFuncZero A holds
( a = 0 & b = 0 )
A5: ( f . x2 = 0 & g . x2 = 1 ) by A2, A3, A4;
A6: ( f . x1 = 1 & g . x1 = 0 ) by A1, A4;
let a, b be Real; :: thesis: ( (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]) = RealFuncZero A implies ( a = 0 & b = 0 ) )
reconsider x1 = x1, x2 = x2 as Element of A by A1, A2;
assume A7: (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]) = RealFuncZero A ; :: thesis: ( a = 0 & b = 0 )
then A8: 0 = ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x2 by FUNCOP_1:13
.= (((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2) by Th10
.= (a * (f . x2)) + (((RealFuncExtMult A) . [b,g]) . x2) by Th15
.= 0 + (b * 1) by A5, Th15
.= b ;
0 = ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) . x1 by A7, FUNCOP_1:13
.= (((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1) by Th10
.= (a * (f . x1)) + (((RealFuncExtMult A) . [b,g]) . x1) by Th15
.= a + (b * 0 ) by A6, Th15
.= a ;
hence ( a = 0 & b = 0 ) by A8; :: thesis: verum