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
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 ; :: 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 A1; :: 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: verum

proof

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;