let x1, x2 be set ; :: thesis: for A being non empty set st x1 in A & x2 in A & x1 <> x2 holds
ex f, g being Element of Funcs (A,COMPLEX) st
for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )
let A be non empty set ; :: thesis: ( x1 in A & x2 in A & x1 <> x2 implies ex f, g being Element of Funcs (A,COMPLEX) st
for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 ) )
assume A1: ( x1 in A & x2 in A & x1 <> x2 ) ; :: thesis: ex f, g being Element of Funcs (A,COMPLEX) st
for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )
consider f, g being Element of Funcs (A,COMPLEX) such that
A2: ( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0c ) ) ) & ( for z being set st z in A holds
( ( z = x1 implies g . z = 0c ) & ( z <> x1 implies g . z = 1r ) ) ) ) by Th17;
take f ; :: thesis: ex g being Element of Funcs (A,COMPLEX) st
for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )
take g ; :: thesis: for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0 & b = 0 )
let a, b be Complex; :: thesis: ( (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A implies ( a = 0 & b = 0 ) )
assume (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A ; :: thesis: ( a = 0 & b = 0 )
hence ( a = 0 & b = 0 ) by A1, A2, Th18; :: thesis: verum