set A = {0 ,1};
take V = RealVectSpace {0 ,1}; :: thesis: ex u, v being Element of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )
consider f, g being Element of Funcs {0 ,1},REAL such that
A2:
( ( for a, b being Real st (RealFuncAdd {0 ,1}) . ((RealFuncExtMult {0 ,1}) . [a,f]),((RealFuncExtMult {0 ,1}) . [b,g]) = RealFuncZero {0 ,1} holds
( a = 0 & b = 0 ) ) & ( for h being Element of Funcs {0 ,1},REAL ex a, b being Real st h = (RealFuncAdd {0 ,1}) . ((RealFuncExtMult {0 ,1}) . [a,f]),((RealFuncExtMult {0 ,1}) . [b,g]) ) )
by Th33;
reconsider u = f, v = g as Element of V ;
take
u
; :: thesis: ex v being Element of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )
take
v
; :: thesis: ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )
thus
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 )
by A2; :: thesis: for w being Element of V ex a, b being Real st w = (a * u) + (b * v)
thus
for w being Element of V ex a, b being Real st w = (a * u) + (b * v)
:: thesis: verumproof
let w be
Element of
V;
:: thesis: ex a, b being Real st w = (a * u) + (b * v)
reconsider h =
w as
Element of
Funcs {0 ,1},
REAL ;
consider a,
b being
Real such that A3:
h = (RealFuncAdd {0 ,1}) . ((RealFuncExtMult {0 ,1}) . [a,f]),
((RealFuncExtMult {0 ,1}) . [b,g])
by A2;
h = (a * u) + (b * v)
by A3;
hence
ex
a,
b being
Real st
w = (a * u) + (b * v)
;
:: thesis: verum
end;