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 Th17;
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 Th17, FUNCT_2:def 1;
hence x is Element of (.: (G,X)) by A1, FUNCT_2:def 2; :: thesis: verum