let x, X be set ; 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 ; ( 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,H3(G)) )
by Th17;
hence
( x is Element of (.: (G,X)) implies x is Function of X,H3(G) )
; ( x is Function of X, the carrier of G implies x is Element of (.: (G,X)) )
assume
x is Function of X,H3(G)
; x is Element of (.: (G,X))
then reconsider f = x as Function of X,H3(G) ;
A1:
rng f c= H3(G)
;
( H3( .: (G,X)) = Funcs (X,H3(G)) & dom f = X )
by Th17, FUNCT_2:def 1;
hence
x is Element of (.: (G,X))
by A1, FUNCT_2:def 2; verum