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

suppose x in dom p ; :: thesis: p . x is Sequence-like

hence p . x is Sequence-like by Def1; :: thesis: verum

end;

suppose not x in dom p ; :: thesis: p . x is Sequence-like

hence p . x is Sequence-like by FUNCT_1:def 2; :: thesis: verum

end;

end;