set Q1 = {(0 const 0),(1 succ 1)};
set Q2 = { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ;
A1: { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } c= HFuncs NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } or x in HFuncs NAT )
assume x in { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ; :: thesis: x in HFuncs NAT
then ex n, i being Element of NAT st
( x = n proj i & 1 <= i & i <= n ) ;
hence x in HFuncs NAT by Th34; :: thesis: verum

end;

{(0 const 0),(1 succ 1)} c= HFuncs NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0 const 0),(1 succ 1)} or x in HFuncs NAT )
assume x in {(0 const 0),(1 succ 1)} ; :: thesis: x in HFuncs NAT
then ( x = 0 const 0 or x = 1 succ 1 ) by TARSKI:def 2;
hence x in HFuncs NAT by Th30, Th32; :: thesis: verum

end;

hence {(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } is Subset of (HFuncs NAT) by A1, XBOOLE_1:8; :: thesis: verum