deffunc H₂( set ) -> set = IFEQ $1,a_Term ,Vars ,{} ;
consider V being ManySortedSet of such that
A1: 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 )
A2: ( IFEQ a_Type ,a_Term ,Vars ,{} = {} & IFEQ an_Adj ,a_Term ,Vars ,{} = {} & IFEQ a_Term ,a_Term ,Vars ,{} = Vars ) by FUNCOP_1:def 8;
( a_Type in the carrier of C & an_Adj in the carrier of C & a_Term in the carrier of C ) by A0, ENUMSET1:def 1;
hence ( V . a_Type = {} & V . an_Adj = {} & V . a_Term = Vars ) by A1, A2; :: thesis: verum