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

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

end;

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