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
then reconsider s = s as Function of [:NAT,NAT:],X by a1, FUNCT_2:3;
take
s
; 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
; 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
; for n, m being Nat holds s . (n,m) = seq . (((id NAT) . n),((id NAT) . m))