now

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