let s, t be XFinSequence; :: thesis: for p being XFinSequence-yielding FinSequence holds
( s ^+ (t ^+ p) = (s ^ t) ^+ p & (p +^ t) +^ s = p +^ (t ^ s) )
let p be XFinSequence-yielding FinSequence; :: thesis: ( s ^+ (t ^+ p) = (s ^ t) ^+ p & (p +^ t) +^ s = p +^ (t ^ s) )

A1: now :: thesis: for k being Nat st k in dom (s ^+ (t ^+ p)) holds
(s ^+ (t ^+ p)) . k = ((s ^ t) ^+ p) . k

let k be Nat; :: thesis: ( k in dom (s ^+ (t ^+ p)) implies (s ^+ (t ^+ p)) . k = ((s ^ t) ^+ p) . k )
assume k in dom (s ^+ (t ^+ p)) ; :: thesis: (s ^+ (t ^+ p)) . k = ((s ^ t) ^+ p) . k
then A2: k in dom (t ^+ p) by Def2;
then A3: k in dom p by Def2;
thus (s ^+ (t ^+ p)) . k = s ^ ((t ^+ p) . k) by A2, Def2
.= s ^ (t ^ (p . k)) by A3, Def2
.= (s ^ t) ^ (p . k) by AFINSQ_1:27
.= ((s ^ t) ^+ p) . k by A3, Def2 ; :: thesis: verum

end;

dom (s ^+ (t ^+ p)) = dom (t ^+ p) by Def2
.= dom p by Def2
.= dom ((s ^ t) ^+ p) by Def2 ;
hence s ^+ (t ^+ p) = (s ^ t) ^+ p by A1, FINSEQ_1:13; :: thesis: (p +^ t) +^ s = p +^ (t ^ s)

A4: now :: thesis: for k being Nat st k in dom ((p +^ t) +^ s) holds
((p +^ t) +^ s) . k = (p +^ (t ^ s)) . k

let k be Nat; :: thesis: ( k in dom ((p +^ t) +^ s) implies ((p +^ t) +^ s) . k = (p +^ (t ^ s)) . k )
assume k in dom ((p +^ t) +^ s) ; :: thesis: ((p +^ t) +^ s) . k = (p +^ (t ^ s)) . k
then A5: k in dom (p +^ t) by Def3;
then A6: k in dom p by Def3;
thus ((p +^ t) +^ s) . k = ((p +^ t) . k) ^ s by A5, Def3
.= ((p . k) ^ t) ^ s by A6, Def3
.= (p . k) ^ (t ^ s) by AFINSQ_1:27
.= (p +^ (t ^ s)) . k by A6, Def3 ; :: thesis: verum

end;

dom ((p +^ t) +^ s) = dom (p +^ t) by Def3
.= dom p by Def3
.= dom (p +^ (t ^ s)) by Def3 ;
hence (p +^ t) +^ s = p +^ (t ^ s) by A4, FINSEQ_1:13; :: thesis: verum