let V be RealLinearSpace; :: thesis: for u, u1, v, v1 being VECTOR of V holds (u # u1) # (v # v1) = (u # v) # (u1 # v1)
let u, u1, v, v1 be VECTOR of V; :: thesis: (u # u1) # (v # v1) = (u # v) # (u1 # v1)
set p = u # u1;
set q = v # v1;
set r = u # v;
set s = u1 # v1;
set x = (u # u1) # (v # v1);
set y = (u # v) # (u1 # v1);

A1: now :: thesis: for w being VECTOR of V holds (w + w) + (w + w) = 4 * w

let w be VECTOR of V; :: thesis: (w + w) + (w + w) = 4 * w
w = 1 * w by RLVECT_1:def 8;
then (w + w) + (w + w) = ((1 + 1) * w) + ((1 * w) + (1 * w)) by RLVECT_1:def 6
.= ((1 + 1) * w) + ((1 + 1) * w) by RLVECT_1:def 6
.= ((1 + 1) + (1 + 1)) * w by RLVECT_1:def 6 ;
hence (w + w) + (w + w) = 4 * w ; :: thesis: verum

end;

(((u # u1) # (v # v1)) + ((u # u1) # (v # v1))) + (((u # u1) # (v # v1)) + ((u # u1) # (v # v1))) = (((u # u1) # (v # v1)) + ((u # u1) # (v # v1))) + ((u # u1) + (v # v1)) by Def2
.= ((u # u1) + (v # v1)) + ((u # u1) + (v # v1)) by Def2
.= (u # u1) + ((v # v1) + ((u # u1) + (v # v1))) by RLVECT_1:def 3
.= (u # u1) + ((u # u1) + ((v # v1) + (v # v1))) by RLVECT_1:def 3
.= ((u # u1) + (u # u1)) + ((v # v1) + (v # v1)) by RLVECT_1:def 3
.= ((u # u1) + (u # u1)) + (v + v1) by Def2
.= (u + u1) + (v + v1) by Def2
.= u + (u1 + (v + v1)) by RLVECT_1:def 3
.= u + (v + (v1 + u1)) by RLVECT_1:def 3
.= (u + v) + (v1 + u1) by RLVECT_1:def 3
.= (u + v) + ((u1 # v1) + (u1 # v1)) by Def2
.= ((u # v) + (u # v)) + ((u1 # v1) + (u1 # v1)) by Def2
.= (u # v) + ((u # v) + ((u1 # v1) + (u1 # v1))) by RLVECT_1:def 3
.= (u # v) + ((u1 # v1) + ((u1 # v1) + (u # v))) by RLVECT_1:def 3
.= ((u # v) + (u1 # v1)) + ((u1 # v1) + (u # v)) by RLVECT_1:def 3
.= (((u # v) # (u1 # v1)) + ((u # v) # (u1 # v1))) + ((u # v) + (u1 # v1)) by Def2
.= (((u # v) # (u1 # v1)) + ((u # v) # (u1 # v1))) + (((u # v) # (u1 # v1)) + ((u # v) # (u1 # v1))) by Def2 ;
then 4 * ((u # u1) # (v # v1)) = (((u # v) # (u1 # v1)) + ((u # v) # (u1 # v1))) + (((u # v) # (u1 # v1)) + ((u # v) # (u1 # v1))) by A1
.= 4 * ((u # v) # (u1 # v1)) by A1 ;
hence (u # u1) # (v # v1) = (u # v) # (u1 # v1) by RLVECT_1:36; :: thesis: verum