let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a, b, c, d being Element of (DTrSpace V,w,y) st Gen w,y holds
(a # b) # (c # d) = (a # c) # (b # d)
let w, y be VECTOR of V; :: thesis: for a, b, c, d being Element of (DTrSpace V,w,y) st Gen w,y holds
(a # b) # (c # d) = (a # c) # (b # d)
let a, b, c, d be Element of (DTrSpace V,w,y); :: thesis: ( Gen w,y implies (a # b) # (c # d) = (a # c) # (b # d) )
assume Gen w,y ; :: thesis: (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 # b = u # u1 & c # d = v # v1 & a # c = u # v & b # d = u1 # v1 ) by Def8;
hence (a # b) # (c # d) = (u # u1) # (v # v1) by Def8
.= (u # v) # (u1 # v1) by Th8
.= (a # c) # (b # d) by A1, Def8 ;
:: thesis: verum