deffunc H₁( object ) -> Subset of X = F_LABEL ($1,X);
A1: for x being object st x in S holds
H₁(x) in bool X ;
consider IT being Function of S,(bool X) such that
A2: for x being object st x in S holds
IT . x = H₁(x) from FUNCT_2:sch 2(A1);
take IT ; :: thesis: for x being object st x in S holds
IT . x = F_LABEL (x,X)
thus for x being object st x in S holds
IT . x = F_LABEL (x,X) by A2; :: thesis: verum