set I = id the carrier of G;

set X = { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st

for x being Element of G holds f . x = x |^ a } ;

A1: ex a being Element of G st

for x being Element of G holds (id the carrier of G) . x = x |^ a

then A3: id the carrier of G in { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st

for x being Element of G holds f . x = x |^ a } by A1;

{ f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st

for x being Element of G holds f . x = x |^ a } is functional

for x being Element of G holds f . x = x |^ a } as functional non empty set by A3;

X is FUNCTION_DOMAIN of the carrier of G, the carrier of G

take X ; :: thesis: for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in X iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a )

let f be Element of Funcs ( the carrier of G, the carrier of G); :: thesis: ( f in X iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a )

for x being Element of G holds f . x = x |^ a implies f in X ) ; :: thesis: verum

set X = { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st

for x being Element of G holds f . x = x |^ a } ;

A1: ex a being Element of G st

for x being Element of G holds (id the carrier of G) . x = x |^ a

proof

id the carrier of G is Element of Funcs ( the carrier of G, the carrier of G)
by FUNCT_2:8;
take a = 1_ G; :: thesis: for x being Element of G holds (id the carrier of G) . x = x |^ a

let x be Element of G; :: thesis: (id the carrier of G) . x = x |^ a

A2: a " = 1_ G by GROUP_1:8;

thus (id the carrier of G) . x = x

.= x * a by GROUP_1:def 4

.= x |^ a by A2, GROUP_1:def 4 ; :: thesis: verum

end;let x be Element of G; :: thesis: (id the carrier of G) . x = x |^ a

A2: a " = 1_ G by GROUP_1:8;

thus (id the carrier of G) . x = x

.= x * a by GROUP_1:def 4

.= x |^ a by A2, GROUP_1:def 4 ; :: thesis: verum

then A3: id the carrier of G in { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st

for x being Element of G holds f . x = x |^ a } by A1;

{ f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st

for x being Element of G holds f . x = x |^ a } is functional

proof

then reconsider X = { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st
let h be object ; :: according to FUNCT_1:def 13 :: thesis: ( not h in { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st

for x being Element of G holds f . x = x |^ a } or h is set )

assume h in { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st

for x being Element of G holds f . x = x |^ a } ; :: thesis: h is set

then ex f being Element of Funcs ( the carrier of G, the carrier of G) st

( f = h & ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ;

hence h is set ; :: thesis: verum

end;for x being Element of G holds f . x = x |^ a } or h is set )

assume h in { f where f is Element of Funcs ( the carrier of G, the carrier of G) : ex a being Element of G st

for x being Element of G holds f . x = x |^ a } ; :: thesis: h is set

then ex f being Element of Funcs ( the carrier of G, the carrier of G) st

( f = h & ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ;

hence h is set ; :: thesis: verum

for x being Element of G holds f . x = x |^ a } as functional non empty set by A3;

X is FUNCTION_DOMAIN of the carrier of G, the carrier of G

proof

then reconsider X = X as FUNCTION_DOMAIN of the carrier of G, the carrier of G ;
let h be Element of X; :: according to FUNCT_2:def 12 :: thesis: h is Element of bool [: the carrier of G, the carrier of G:]

h in X ;

then ex f being Element of Funcs ( the carrier of G, the carrier of G) st

( f = h & ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ;

hence h is Element of bool [: the carrier of G, the carrier of G:] ; :: thesis: verum

end;h in X ;

then ex f being Element of Funcs ( the carrier of G, the carrier of G) st

( f = h & ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ;

hence h is Element of bool [: the carrier of G, the carrier of G:] ; :: thesis: verum

take X ; :: thesis: for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in X iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a )

let f be Element of Funcs ( the carrier of G, the carrier of G); :: thesis: ( f in X iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a )

hereby :: thesis: ( ex a being Element of G st

for x being Element of G holds f . x = x |^ a implies f in X )

thus
( ex a being Element of G st for x being Element of G holds f . x = x |^ a implies f in X )

assume
f in X
; :: thesis: ex a being Element of G st

for x being Element of G holds f . x = x |^ a

then ex f1 being Element of Funcs ( the carrier of G, the carrier of G) st

( f1 = f & ex a being Element of G st

for x being Element of G holds f1 . x = x |^ a ) ;

hence ex a being Element of G st

for x being Element of G holds f . x = x |^ a ; :: thesis: verum

end;for x being Element of G holds f . x = x |^ a

then ex f1 being Element of Funcs ( the carrier of G, the carrier of G) st

( f1 = f & ex a being Element of G st

for x being Element of G holds f1 . x = x |^ a ) ;

hence ex a being Element of G st

for x being Element of G holds f . x = x |^ a ; :: thesis: verum

for x being Element of G holds f . x = x |^ a implies f in X ) ; :: thesis: verum