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