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

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;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