let x, X be set ; :: thesis: for G being non empty multMagma holds
( x is Element of (.: G,X) iff x is Function of X,the carrier of G )
let G be non empty multMagma ; :: thesis: ( x is Element of (.: G,X) iff x is Function of X,the carrier of G )
( x is Element of (.: G,X) implies x is Element of Funcs X,H₃(G) ) by Th18;
hence ( x is Element of (.: G,X) implies x is Function of X,H₃(G) ) ; :: thesis: ( x is Function of X,the carrier of G implies x is Element of (.: G,X) )
assume x is Function of X,H₃(G) ; :: thesis: x is Element of (.: G,X)
then reconsider f = x as Function of X,H₃(G) ;
A1: rng f c= H₃(G) ;
( H₃( .: G,X) = Funcs X,H₃(G) & dom f = X ) by Th18, FUNCT_2:def 1;
hence x is Element of (.: G,X) by A1, FUNCT_2:def 2; :: thesis: verum