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 (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 h' being Element of Funcs A,REAL ex a, b, c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h]) ) ) by A1, Th15;
reconsider u = f, v = g, w = h as Element of (RealVectSpace A) ;
A3: for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. (RealVectSpace A) holds
( a = 0 & b = 0 & c = 0 ) by A2;
A4: for y being Element of (RealVectSpace A) ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w)

proof

let y be Element of (RealVectSpace A); :: thesis: ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w)
reconsider h' = y as Element of Funcs A,REAL ;
consider a, b, c being Real such that
A5: h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h]) by A2;
h' = ((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

end;

not u is zero by A3, Th1;
then u <> 0. (RealVectSpace A) by STRUCT_0:def 15;
then reconsider V = RealVectSpace A as non trivial RealLinearSpace by STRUCT_0:def 19;
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 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) by A2, A4; :: thesis: verum