set A = {0,1};
take V = RealVectSpace {0,1}; 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
A1:
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 )
and
A2:
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 Th22;
reconsider u = f, v = g as Element of V ;
take
u
; 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
; ( ( 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 A1; 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)
verumproof
let w be
Element of
V;
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)
;
verum
end;