let V be RealLinearSpace; for w, y being VECTOR of V
for a, b, c, d being Element of (DTrSpace (V,w,y)) holds (a # b) # (c # d) = (a # c) # (b # d)
let w, y be VECTOR of V; for a, b, c, d being Element of (DTrSpace (V,w,y)) holds (a # b) # (c # d) = (a # c) # (b # d)
let a, b, c, d be Element of (DTrSpace (V,w,y)); (a # b) # (c # d) = (a # c) # (b # d)
reconsider u = a, u1 = b, v = c, v1 = d as VECTOR of V ;
set ab = a # b;
set cd = c # d;
set ac = a # c;
set bd = b # d;
set uu1 = u # u1;
set vv1 = v # v1;
set uv = u # v;
set u1v1 = u1 # v1;
A1:
( a # c = u # v & b # d = u1 # v1 )
by Def8;
( a # b = u # u1 & c # d = v # v1 )
by Def8;
hence (a # b) # (c # d) =
(u # u1) # (v # v1)
by Def8
.=
(u # v) # (u1 # v1)
by Th6
.=
(a # c) # (b # d)
by A1, Def8
;
verum