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
proof
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;
id the carrier of G is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
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
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;
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
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
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;
then reconsider X = X as 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 )
hereby :: thesis: ( 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;
thus ( ex a being Element of G st
for x being Element of G holds f . x = x |^ a implies f in X ) ; :: thesis: verum