let S1, S2 be Element of (V . W); :: thesis: ( ( for a being Vector of V st S = a . W holds
S1 = (r * a) . W ) & ( for a being Vector of V st S = a . W holds
S2 = (r * a) . W ) implies S1 = S2 )
assume that
A3: for a being Vector of V st S = a . W holds
S1 = (r * a) . W and
A4: for a being Vector of V st S = a . W holds
S2 = (r * a) . W ; :: thesis: S1 = S2
consider a1 being Vector of V such that
A5: S = a1 . W by Th22;
thus S1 = (r * a1) . W by A3, A5
.= S2 by A4, A5 ; :: thesis: verum