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 object ; :: 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 ex f being Element of HFuncs NAT ex F being with_the_same_arity Element of (HFuncs NAT) * st
( x = f * <:F:> & f in Q & arity f = len F & rng F c= Q ) ;
hence x in HFuncs NAT by Th41; :: 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