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,REAL) st
( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) )
let A be non empty set ; :: thesis: ( A = {x1,x2} & x1 <> x2 implies ex f, g being Element of Funcs (A,REAL) st
( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) ) )
assume that
A1: A = {x1,x2} and
A2: x1 <> x2 ; :: thesis: ex f, g being Element of Funcs (A,REAL) st
( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) )
x1 in A by TARSKI:def 2, A1;
then reconsider f = (RealFuncZero A) +* (x1 .--> 1), g = (RealFuncUnit A) +* (x1 .--> 0) as Element of Funcs (A,REAL) by Th17;
take f ; :: thesis: ex g being Element of Funcs (A,REAL) st
( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) )
take g ; :: thesis: ( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) )
( x1 in A & x2 in A ) by A1, TARSKI:def 2;
hence ( ( for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,REAL) ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) ) ) by A1, A2, Th18, Th20; :: thesis: verum