let D be set ; :: thesis: for f, g being XFinSequence of D
for h being FinSequence of D holds
( (f ^ g) ^ h = f ^ (g ^ h) & (f ^ h) ^ g = f ^ (h ^ g) & (h ^ f) ^ g = h ^ (f ^ g) )
let f, g be XFinSequence of D; :: thesis: for h being FinSequence of D holds
( (f ^ g) ^ h = f ^ (g ^ h) & (f ^ h) ^ g = f ^ (h ^ g) & (h ^ f) ^ g = h ^ (f ^ g) )
let h be FinSequence of D; :: thesis: ( (f ^ g) ^ h = f ^ (g ^ h) & (f ^ h) ^ g = f ^ (h ^ g) & (h ^ f) ^ g = h ^ (f ^ g) )
L1: (f ^ g) ^ h = (f ^ g) ^ (FS2XFS h) by XFF
.= f ^ (g ^ (FS2XFS h)) by AFINSQ_1:27
.= f ^ (g ^ h) by XFF ;
L2: (f ^ h) ^ g = (f ^ (XFS2FS (FS2XFS h))) ^ g
.= (f ^ (FS2XFS h)) ^ g by XFX
.= f ^ ((FS2XFS h) ^ (FS2XFS (XFS2FS g))) by AFINSQ_1:27
.= f ^ (FS2XFS (h ^ (XFS2FS g))) by SFF
.= f ^ (h ^ (XFS2FS g)) by XFF
.= f ^ (h ^ g) by FFX ;
(h ^ f) ^ g = (h ^ (FS2XFS (XFS2FS f))) ^ (XFS2FS (FS2XFS (XFS2FS g))) by FFX
.= (h ^ (XFS2FS f)) ^ (XFS2FS g) by FFX
.= h ^ ((XFS2FS f) ^ (XFS2FS g)) by FINSEQ_1:32
.= h ^ (XFS2FS (f ^ g)) by SXX
.= h ^ (f ^ g) by FFX ;
hence ( (f ^ g) ^ h = f ^ (g ^ h) & (f ^ h) ^ g = f ^ (h ^ g) & (h ^ f) ^ g = h ^ (f ^ g) ) by L1, L2; :: thesis: verum