let A be non empty set ; :: thesis: for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 holds
ex f, g, h being Element of Funcs (A,REAL) st
( ( for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) ) )
let x1, x2, x3 be Element of A; :: thesis: ( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 implies ex f, g, h being Element of Funcs (A,REAL) st
( ( for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) ) ) )
assume A1: ( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 ) ; :: thesis: ex f, g, h being Element of Funcs (A,REAL) st
( ( for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) ) )
consider f being Element of Funcs (A,REAL) such that
A2: ( f . x1 = 1 & ( for z being set st z in A & z <> x1 holds
f . z = 0 ) ) by Th10;
consider h being Element of Funcs (A,REAL) such that
A3: ( h . x3 = 1 & ( for z being set st z in A & z <> x3 holds
h . z = 0 ) ) by Th10;
consider g being Element of Funcs (A,REAL) such that
A4: ( g . x2 = 1 & ( for z being set st z in A & z <> x2 holds
g . z = 0 ) ) by Th10;
take f ; :: thesis: ex g, h being Element of Funcs (A,REAL) st
( ( for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) ) )
take g ; :: thesis: ex h being Element of Funcs (A,REAL) st
( ( for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) ) )
take h ; :: thesis: ( ( for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) ) )
thus ( ( for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 ) ) & ( for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) ) ) by A1, A2, A4, A3, Th11, Th13; :: thesis: verum