per cases ( k in dom p or not k in dom p ) ;

suppose k in dom p ; :: thesis: p . k is Element of E ^omega

hence p . k is Element of E ^omega by FINSEQ_2:11; :: thesis: verum

end;

suppose not k in dom p ; :: thesis: p . k is Element of E ^omega

then p . k = {} by FUNCT_1:def 2;
then p . k is XFinSequence of E by AFINSQ_1:16;
hence p . k is Element of E ^omega by AFINSQ_1:def 7; :: thesis: verum

end;

end;