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 )
A1: H₃( .: G,X) = Funcs X,H₃(G) by Th18;
( 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) ;
( dom f = X & rng f c= H₃(G) ) by FUNCT_2:def 1;
hence x is Element of (.: G,X) by A1, FUNCT_2:def 2; :: thesis: verum