let x1, x2 be set ; :: thesis: for A being non empty set st A = {x1,x2} & 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 ) ) & ( for h being Element of Funcs A,COMPLEX ex a, b being Complex st h = (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) ) )
let A be non empty set ; :: thesis: ( A = {x1,x2} & 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 ) ) & ( for h being Element of Funcs A,COMPLEX ex a, b being Complex st h = (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) ) ) )
assume A1: ( A = {x1,x2} & 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 ) ) & ( for h being Element of Funcs A,COMPLEX ex a, b being Complex st h = (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) ) )
then A2: ( x1 in A & x2 in A & x1 <> x2 ) by TARSKI:def 2;
consider f, g being Element of Funcs A,COMPLEX such that
A3: for z being set st z in A holds
( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0c ) ) and
A4: for z being set st z in A holds
( ( z = x1 implies g . z = 0c ) & ( z <> x1 implies g . z = 1r ) ) by Th19;
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 ) ) & ( for h being Element of Funcs A,COMPLEX ex a, b being Complex st h = (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) ) )
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 ) ) & ( for h being Element of Funcs A,COMPLEX ex a, b being Complex st h = (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) ) )
thus ( ( for a, b being Complex st (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) = ComplexFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs A,COMPLEX ex a, b being Complex st h = (ComplexFuncAdd A) . ((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]) ) ) by A1, A2, A3, A4, Th20, Th22; :: thesis: verum