let o be operation of S; :: thesis: o is quasi_total

consider i being object such that

A1: ( i in dom the charact of S & o = the charact of S . i ) by FUNCT_1:def 3;

thus o is quasi_total by A1, MARGREL1:def 24; :: thesis: verum

consider i being object such that

A1: ( i in dom the charact of S & o = the charact of S . i ) by FUNCT_1:def 3;

thus o is quasi_total by A1, MARGREL1:def 24; :: thesis: verum