now

let i be Nat; :: thesis: ( i in dom (s ^+ p) implies (s ^+ p) . i in E ^omega )
assume A1: i in dom (s ^+ p) ; :: thesis: (s ^+ p) . i in E ^omega
i in dom p by A1, Def2;
then (s ^+ p) . i = s ^ (p . i) by Def2;
hence (s ^+ p) . i in E ^omega ; :: thesis: verum

end;

hence s ^+ p is FinSequence of E ^omega by FINSEQ_2:14; :: thesis: verum