now :: thesis: for i being Nat st i in dom (s ^+ p) holds
(s ^+ p) . i in E ^omega

let i be Nat; :: thesis: ( i in dom (s ^+ p) implies (s ^+ p) . i in E ^omega )
assume i in dom (s ^+ p) ; :: thesis: (s ^+ p) . i in E ^omega
then i in dom p by 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:12; :: thesis: verum