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 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 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 A1: ( A = {x1,x2} & x1 <> x2 ) ; :: thesis: ex f, g being Element of Funcs A,REAL st
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])
consider f, g being Element of Funcs A,REAL such that
A2: for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( 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 = 1 ) ) by Th28;
take f ; :: thesis: ex g being Element of Funcs A,REAL st
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 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 h be Element of Funcs A,REAL ; :: thesis: ex a, b being Real st h = (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])
thus ex a, b being Real st h = (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]) by A1, A2, A3, Th31; :: thesis: verum