consider A being non empty set , x1, x2, x3, x4 being Element of A such that

A1: ( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 ) by Lm31;

set V = RealVectSpace A;

consider f, g, h, f1 being Element of Funcs (A,REAL) such that

A2: for a, b, c, d being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 & d = 0 ) and

A3: for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) by A1, Th21;

reconsider u = f, v = g, w = h, u1 = f1 as Element of (RealVectSpace A) ;

for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. (RealVectSpace A) holds

( a = 0 & b = 0 & c = 0 & d = 0 ) by A2;

then not u is zero by Th2;

then A4: u <> 0. (RealVectSpace A) ;

A5: for y being Element of (RealVectSpace A) ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1)

take V ; :: thesis: ex u, v, w, u1 being Element of V st

( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

reconsider u = u, v = v, w = w, u1 = u1 as Element of V ;

take u ; :: thesis: ex v, w, u1 being Element of V st

( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

take v ; :: thesis: ex w, u1 being Element of V st

( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

take w ; :: thesis: ex u1 being Element of V st

( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

take u1 ; :: thesis: ( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

thus for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) by A2; :: thesis: for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1)

let y be Element of V; :: thesis: ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1)

ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) by A5;

hence ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ; :: thesis: verum

A1: ( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 ) by Lm31;

set V = RealVectSpace A;

consider f, g, h, f1 being Element of Funcs (A,REAL) such that

A2: for a, b, c, d being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) = RealFuncZero A holds

( a = 0 & b = 0 & c = 0 & d = 0 ) and

A3: for h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) by A1, Th21;

reconsider u = f, v = g, w = h, u1 = f1 as Element of (RealVectSpace A) ;

for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. (RealVectSpace A) holds

( a = 0 & b = 0 & c = 0 & d = 0 ) by A2;

then not u is zero by Th2;

then A4: u <> 0. (RealVectSpace A) ;

A5: for y being Element of (RealVectSpace A) ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1)

proof

reconsider V = RealVectSpace A as non trivial RealLinearSpace by A4, STRUCT_0:def 18;
let y be Element of (RealVectSpace A); :: thesis: ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1)

reconsider h9 = y as Element of Funcs (A,REAL) ;

consider a, b, c, d being Real such that

A6: h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) by A3;

h9 = (((a * u) + (b * v)) + (c * w)) + (d * u1) by A6;

hence ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ; :: thesis: verum

end;reconsider h9 = y as Element of Funcs (A,REAL) ;

consider a, b, c, d being Real such that

A6: h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1])) by A3;

h9 = (((a * u) + (b * v)) + (c * w)) + (d * u1) by A6;

hence ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ; :: thesis: verum

take V ; :: thesis: ex u, v, w, u1 being Element of V st

( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

reconsider u = u, v = v, w = w, u1 = u1 as Element of V ;

take u ; :: thesis: ex v, w, u1 being Element of V st

( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

take v ; :: thesis: ex w, u1 being Element of V st

( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

take w ; :: thesis: ex u1 being Element of V st

( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

take u1 ; :: thesis: ( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )

thus for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds

( a = 0 & b = 0 & c = 0 & d = 0 ) by A2; :: thesis: for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1)

let y be Element of V; :: thesis: ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1)

ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) by A5;

hence ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ; :: thesis: verum