let x1, x2 be set ; :: thesis: for A being non empty set
for f, g being Element of Funcs A,COMPLEX st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( 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 = 1r ) ) ) holds
for a, b being Complex st (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) = ComplexFuncZero A holds
( a = 0c & b = 0c )
let A be non empty set ; :: thesis: for f, g being Element of Funcs A,COMPLEX st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( 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 = 1r ) ) ) holds
for a, b being Complex st (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) = ComplexFuncZero A holds
( a = 0c & b = 0c )
let f, g be Element of Funcs A,COMPLEX ; :: thesis: ( x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( 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 = 1r ) ) ) implies for a, b being Complex st (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) = ComplexFuncZero A holds
( a = 0c & b = 0c ) )
assume that
A1: ( x1 in A & x2 in A & x1 <> x2 ) and
A2: for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) and
A3: for z being set st z in A holds
( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ; :: thesis: for a, b being Complex st (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) = ComplexFuncZero A holds
( a = 0c & b = 0c )
A4: ( f . x1 = 1r & f . x2 = 0c & g . x1 = 0c & g . x2 = 1r ) by A1, A2, A3;
reconsider x1 = x1, x2 = x2 as Element of A by A1;
let a, b be Complex; :: thesis: ( (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) = ComplexFuncZero A implies ( a = 0c & b = 0c ) )
assume A5: (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) = ComplexFuncZero A ; :: thesis: ( a = 0c & b = 0c )
then A6: 0c = ((ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) . x1 by FUNCOP_1:13
.= (((ComplexFuncExtMult A) . [a,f]) . x1) + (((ComplexFuncExtMult A) . [b,g]) . x1) by Th1
.= (a * (f . x1)) + (((ComplexFuncExtMult A) . [b,g]) . x1) by Th6
.= a + (b * 0c ) by A4, Th6, COMPLEX1:def 7
.= a ;
0c = ((ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) . x2 by A5, FUNCOP_1:13
.= (((ComplexFuncExtMult A) . [a,f]) . x2) + (((ComplexFuncExtMult A) . [b,g]) . x2) by Th1
.= (a * (f . x2)) + (((ComplexFuncExtMult A) . [b,g]) . x2) by Th6
.= 0c + (b * 1r ) by A4, Th6
.= b by COMPLEX1:def 7 ;
hence ( a = 0c & b = 0c ) by A6; :: thesis: verum