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 Th15;

thus S1 = (r * a1) . W by A3, A5

.= S2 by A4, A5 ; :: thesis: verum

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 Th15;

thus S1 = (r * a1) . W by A3, A5

.= S2 by A4, A5 ; :: thesis: verum