deffunc H₂( object ) -> set = IFEQ ($1,a_Term,Vars,{});
consider V being ManySortedSet of the carrier of C such that
A8: for x being object st x in the carrier of C holds
V . x = H₂(x) from PBOOLE:sch 4();
take V ; :: thesis: ( V . a_Type = {} & V . an_Adj = {} & V . a_Term = Vars )
A9: IFEQ (a_Type,a_Term,Vars,{}) = {} by FUNCOP_1:def 8;
A10: IFEQ (an_Adj,a_Term,Vars,{}) = {} by FUNCOP_1:def 8;
A11: IFEQ (a_Term,a_Term,Vars,{}) = Vars by FUNCOP_1:def 8;
A12: a_Type in the carrier of C by A1, ENUMSET1:def 1;
A13: an_Adj in the carrier of C by A1, ENUMSET1:def 1;
a_Term in the carrier of C by A1, ENUMSET1:def 1;
hence ( V . a_Type = {} & V . an_Adj = {} & V . a_Term = Vars ) by A8, A9, A10, A11, A12, A13; :: thesis: verum