let n be Nat; :: thesis: for X being natural-membered set holds multRel (X,n) = ((curry multnat) . n) |_2 X
let X be natural-membered set ; :: thesis: multRel (X,n) = ((curry multnat) . n) |_2 X
set g = (curry multnat) . n;

now :: thesis: for x, y being object holds
( ( [x,y] in multRel (X,n) implies [x,y] in ((curry multnat) . n) |_2 X ) & ( [x,y] in ((curry multnat) . n) |_2 X implies [x,y] in multRel (X,n) ) )

let x, y be object ; :: thesis: ( ( [x,y] in multRel (X,n) implies [x,y] in ((curry multnat) . n) |_2 X ) & ( [x,y] in ((curry multnat) . n) |_2 X implies [x,y] in multRel (X,n) ) )
reconsider a = x, b = y as set by TARSKI:1;

hereby :: thesis: ( [x,y] in ((curry multnat) . n) |_2 X implies [x,y] in multRel (X,n) )

assume A1: [x,y] in multRel (X,n) ; :: thesis: [x,y] in ((curry multnat) . n) |_2 X
then [a,b] in multRel (X,n) ;
then ( a in X & b in X ) by MMLQUER2:4;
then reconsider a = a, b = b as Integer ;
[a,b] in multRel (X,n) by A1;
then A2: ( a in X & b in X & b = n * a ) by Th42;
then ( n in NAT & a in NAT ) by ORDINAL1:def 12;
then [n,a] in [:NAT,NAT:] by ZFMISC_1:87;
then A3: [n,a] in dom multnat by FUNCT_2:def 1;
A4: b = multnat . (n,a) by A2, BINOP_2:def 24
.= ((curry multnat) . n) . a by A3, FUNCT_5:20 ;
a in dom ((curry multnat) . n) by A3, FUNCT_5:20;
hence [x,y] in ((curry multnat) . n) |_2 X by A2, A4, FUNCT_1:1, MMLQUER2:4; :: thesis: verum

end;

assume [x,y] in ((curry multnat) . n) |_2 X ; :: thesis: [x,y] in multRel (X,n)
then [a,b] in ((curry multnat) . n) |_2 X ;
then A5: ( a in X & b in X & [a,b] in (curry multnat) . n ) by MMLQUER2:4;
then reconsider a = a, b = b as Integer ;
A6: ( n in NAT & a in NAT ) by A5, ORDINAL1:def 12;
then [n,a] in [:NAT,NAT:] by ZFMISC_1:87;
then A7: [n,a] in dom multnat by FUNCT_2:def 1;
( a in dom ((curry multnat) . n) & ((curry multnat) . n) . a = b ) by A5, FUNCT_1:1;
then b = multnat . (n,a) by A7, FUNCT_5:20
.= n * a by A6, BINOP_2:def 24 ;
hence [x,y] in multRel (X,n) by A5, Th42; :: thesis: verum

end;

hence multRel (X,n) = ((curry multnat) . n) |_2 X by RELAT_1:def 2; :: thesis: verum