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

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

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

end;

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