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
.= s ^ (t ^ (p . k)) by
.= (s ^ t) ^ (p . k) by AFINSQ_1:27
.= ((s ^ t) ^+ p) . k by ; :: 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 ; :: 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
.= ((p . k) ^ t) ^ s by
.= (p . k) ^ (t ^ s) by AFINSQ_1:27
.= (p +^ (t ^ s)) . k by ; :: 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 ; :: thesis: verum