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_{3}(G)) )
by Th17;

hence ( x is Element of (.: (G,X)) implies x is Function of X,H_{3}(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_{3}(G)
; :: thesis: x is Element of (.: (G,X))

then reconsider f = x as Function of X,H_{3}(G) ;

A1: rng f c= H_{3}(G)
;

( H_{3}( .: (G,X)) = Funcs (X,H_{3}(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

( 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

hence ( x is Element of (.: (G,X)) implies x is Function of X,H

assume x is Function of X,H

then reconsider f = x as Function of X,H

A1: rng f c= H

( H

hence x is Element of (.: (G,X)) by A1, FUNCT_2:def 2; :: thesis: verum