let x be set ; :: according to MATRLIN:def 1 :: thesis: ( not x in dom (i |-> f) or (i |-> f) . x is set )
assume x in dom (i |-> f) ; :: thesis: (i |-> f) . x is set
then x in Seg i by FUNCOP_1:19;
hence (i |-> f) . x is set by FUNCOP_1:13; :: thesis: verum