let E be set ; :: thesis: for p being XFinSequence-yielding FinSequence holds
( (<%> E) ^+ p = p & p +^ (<%> E) = p )
let p be XFinSequence-yielding FinSequence; :: thesis: ( (<%> E) ^+ p = p & p +^ (<%> E) = p )

A1: now :: thesis: for k being Nat st k in dom p holds
((<%> E) ^+ p) . k = p . k

let k be Nat; :: thesis: ( k in dom p implies ((<%> E) ^+ p) . k = p . k )
assume k in dom p ; :: thesis: ((<%> E) ^+ p) . k = p . k
hence ((<%> E) ^+ p) . k = {} ^ (p . k) by Def2
.= p . k ;
:: thesis: verum

end;

dom ((<%> E) ^+ p) = dom p by Def2;
hence (<%> E) ^+ p = p by A1, FINSEQ_1:13; :: thesis: p +^ (<%> E) = p

A2: now :: thesis: for k being Nat st k in dom p holds
(p +^ (<%> E)) . k = p . k

let k be Nat; :: thesis: ( k in dom p implies (p +^ (<%> E)) . k = p . k )
assume k in dom p ; :: thesis: (p +^ (<%> E)) . k = p . k
hence (p +^ (<%> E)) . k = (p . k) ^ {} by Def3
.= p . k ;
:: thesis: verum

end;

dom (p +^ (<%> E)) = dom p by Def3;
hence p +^ (<%> E) = p by A2, FINSEQ_1:13; :: thesis: verum