let G, F be finite commutative Group; :: thesis: for a being Element of G

for f being Homomorphism of G,F holds the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})

let a be Element of G; :: thesis: for f being Homomorphism of G,F holds the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})

let f be Homomorphism of G,F; :: thesis: the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})

for y being object holds

( y in the carrier of (gr {(f . a)}) iff y in f .: the carrier of (gr {a}) )

for f being Homomorphism of G,F holds the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})

let a be Element of G; :: thesis: for f being Homomorphism of G,F holds the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})

let f be Homomorphism of G,F; :: thesis: the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})

for y being object holds

( y in the carrier of (gr {(f . a)}) iff y in f .: the carrier of (gr {a}) )

proof

hence
the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})
by TARSKI:2; :: thesis: verum
let y be object ; :: thesis: ( y in the carrier of (gr {(f . a)}) iff y in f .: the carrier of (gr {a}) )

then consider x being object such that

AA2: ( x in dom f & x in the carrier of (gr {a}) & y = f . x ) by FUNCT_1:def 6;

reconsider x0 = x as Element of G by AA2;

x0 in gr {a} by AA2;

then consider i being Element of NAT such that

AA3: x0 = a |^ i by GRCY26;

f . x0 = (f . a) |^ i by AA3, GROUP_6:37;

then f . x0 in gr {(f . a)} by GRCY26;

hence y in the carrier of (gr {(f . a)}) by AA2; :: thesis: verum

end;hereby :: thesis: ( y in f .: the carrier of (gr {a}) implies y in the carrier of (gr {(f . a)}) )

assume
y in f .: the carrier of (gr {a})
; :: thesis: y in the carrier of (gr {(f . a)})assume AA1:
y in the carrier of (gr {(f . a)})
; :: thesis: y in f .: the carrier of (gr {a})

then reconsider y0 = y as Element of F by TARSKI:def 3, GROUP_2:def 5;

y0 in gr {(f . a)} by AA1;

then consider i being Element of NAT such that

AA2: y0 = (f . a) |^ i by GRCY26;

AA3: y0 = f . (a |^ i) by AA2, GROUP_6:37;

a |^ i in gr {a} by GRCY26;

hence y in f .: the carrier of (gr {a}) by AA3, FUNCT_2:35; :: thesis: verum

end;then reconsider y0 = y as Element of F by TARSKI:def 3, GROUP_2:def 5;

y0 in gr {(f . a)} by AA1;

then consider i being Element of NAT such that

AA2: y0 = (f . a) |^ i by GRCY26;

AA3: y0 = f . (a |^ i) by AA2, GROUP_6:37;

a |^ i in gr {a} by GRCY26;

hence y in f .: the carrier of (gr {a}) by AA3, FUNCT_2:35; :: thesis: verum

then consider x being object such that

AA2: ( x in dom f & x in the carrier of (gr {a}) & y = f . x ) by FUNCT_1:def 6;

reconsider x0 = x as Element of G by AA2;

x0 in gr {a} by AA2;

then consider i being Element of NAT such that

AA3: x0 = a |^ i by GRCY26;

f . x0 = (f . a) |^ i by AA3, GROUP_6:37;

then f . x0 in gr {(f . a)} by GRCY26;

hence y in the carrier of (gr {(f . a)}) by AA2; :: thesis: verum