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)
proof
let y be
Element of
(RealVectSpace A);
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)
;
verum
end;
reconsider V = RealVectSpace A as non trivial RealLinearSpace by A4, STRUCT_0:def 18;
take
V
; 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
; 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
; 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
; 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
; ( ( 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; 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; 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)
; verum