consider A being non empty set , x1, x2, x3 being Element of A such that
A1: ( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 ) by Lm30;
set V = RealVectSpace A;
consider f, g, h being Element of Funcs (A,REAL) such that
A2: for a, b, c being Real st () . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 ) and
A3: for h9 being Element of Funcs (A,REAL) ex a, b, c being Real st h9 = () . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h])) by ;
reconsider u = f, v = g, w = h as Element of () ;
for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. () holds
( a = 0 & b = 0 & c = 0 ) by A2;
then not u is zero by Th1;
then A4: u <> 0. () ;
A5: for y being Element of () ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w)
proof
let y be Element of (); :: thesis: ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w)
reconsider h9 = y as Element of Funcs (A,REAL) ;
consider a, b, c being Real such that
A6: h9 = () . ((() . ((() . [a,f]),(() . [b,g]))),(() . [c,h])) by A3;
h9 = ((a * u) + (b * v)) + (c * w) by A6;
hence ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ; :: thesis: verum
end;
reconsider V = RealVectSpace A as non trivial RealLinearSpace by ;
take V ; :: thesis: ex u, v, w being Element of V st
( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) )

reconsider u = u, v = v, w = w as Element of V ;
take u ; :: thesis: ex v, w being Element of V st
( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) )

take v ; :: thesis: ex w being Element of V st
( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) )

take w ; :: thesis: ( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) )

thus for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) by A2; :: thesis: for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w)
let y be Element of V; :: thesis: ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w)
ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) by A5;
hence ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ; :: thesis: verum