deffunc H1( object , object ) -> set = seq . (((id NAT) . $1),((id NAT) . $2));
consider s being Function such that
a1: ( dom s = [:NAT,NAT:] & ( for n, m being object st n in NAT & m in NAT holds
s . (n,m) = H1(n,m) ) ) from FUNCT_3:sch 2();
 for z being object st z in [:NAT,NAT:] holds
s . z in X
proof
let z be object ; :: thesis: ( z in [:NAT,NAT:] implies s . z in X )
assume z in [:NAT,NAT:] ; :: thesis: s . z in X
then consider n, m being object such that
a2: ( n in NAT & m in NAT & z = [n,m] ) by ZFMISC_1:def 2;
reconsider n = n, m = m as Nat by a2;
s . z = s . (n,m) by a2;
then s . z = seq . (((id NAT) . n),((id NAT) . m)) by a1, a2;
hence s . z in X ; :: thesis: verum
end;
then reconsider s = s as Function of [:NAT,NAT:],X by a1, FUNCT_2:3;
take s ; :: thesis: ex N, M being V113() sequence of NAT st
for n, m being Nat holds s . (n,m) = seq . ((N . n),(M . m))
take id NAT ; :: thesis: ex M being V113() sequence of NAT st
for n, m being Nat holds s . (n,m) = seq . (((id NAT) . n),(M . m))
take id NAT ; :: thesis: for n, m being Nat holds s . (n,m) = seq . (((id NAT) . n),((id NAT) . m))
hereby :: thesis: verum
let n, m be Nat; :: thesis: s . (n,m) = seq . (((id NAT) . n),((id NAT) . m))
( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;
hence s . (n,m) = seq . (((id NAT) . n),((id NAT) . m)) by a1; :: thesis: verum
end;