set Q1 = { (f * <:F:>) where f is Element of HFuncs NAT , F is with_the_same_arity Element of (HFuncs NAT ) * : ( f in Q & arity f = len F & rng F c= Q ) } ;
{ (f * <:F:>) where f is Element of HFuncs NAT , F is with_the_same_arity Element of (HFuncs NAT ) * : ( f in Q & arity f = len F & rng F c= Q ) } c= HFuncs NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f * <:F:>) where f is Element of HFuncs NAT , F is with_the_same_arity Element of (HFuncs NAT ) * : ( f in Q & arity f = len F & rng F c= Q ) } or x in HFuncs NAT )
assume x in { (f * <:F:>) where f is Element of HFuncs NAT , F is with_the_same_arity Element of (HFuncs NAT ) * : ( f in Q & arity f = len F & rng F c= Q ) } ; :: thesis: x in HFuncs NAT
then consider f being Element of HFuncs NAT , F being with_the_same_arity Element of (HFuncs NAT ) * such that
A4: x = f * <:F:> and
( f in Q & arity f = len F & rng F c= Q ) ;
thus x in HFuncs NAT by A4, Th46; :: thesis: verum

end;

hence Q \/ { (f * <:F:>) where f is Element of HFuncs NAT , F is with_the_same_arity Element of (HFuncs NAT ) * : ( f in Q & arity f = len F & rng F c= Q ) } is Subset of (HFuncs NAT ) by XBOOLE_1:8; :: thesis: verum