deffunc H₂( set ) -> set = IFEQ $1,a_Term ,Vars ,{} ;
consider V being ManySortedSet of the carrier of C such that
A8: for x being set 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