let G, A be Group; for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G holds ((incl1 (G,A,phi)) . g) |^ ((incl2 (G,A,phi)) . a) = <*((phi . (a ")) . g),(1_ A)*>
let phi be Homomorphism of A,(AutGroup G); for a being Element of A
for g being Element of G holds ((incl1 (G,A,phi)) . g) |^ ((incl2 (G,A,phi)) . a) = <*((phi . (a ")) . g),(1_ A)*>
let a be Element of A; for g being Element of G holds ((incl1 (G,A,phi)) . g) |^ ((incl2 (G,A,phi)) . a) = <*((phi . (a ")) . g),(1_ A)*>
let g be Element of G; ((incl1 (G,A,phi)) . g) |^ ((incl2 (G,A,phi)) . a) = <*((phi . (a ")) . g),(1_ A)*>
set xg = (incl1 (G,A,phi)) . g;
set xa = (incl2 (G,A,phi)) . a;
reconsider phi1 = phi . (a ") as Homomorphism of G,G by AUTGROUP:def 1;
A1:
(incl2 (G,A,phi)) . a = <*(1_ G),a*>
by Def3;
then A2: ((incl2 (G,A,phi)) . a) " =
<*(phi1 . ((1_ G) ")),(a ")*>
by Th22
.=
<*(phi1 . (1_ G)),(a ")*>
by GROUP_1:8
.=
<*(1_ G),(a ")*>
by GROUP_6:31
;
(incl1 (G,A,phi)) . g = <*g,(1_ A)*>
by Def2;
then (((incl2 (G,A,phi)) . a) ") * ((incl1 (G,A,phi)) . g) =
<*((1_ G) * (phi1 . g)),((a ") * (1_ A))*>
by A2, Th14
.=
<*((1_ G) * (phi1 . g)),(a ")*>
by GROUP_1:def 4
.=
<*(phi1 . g),(a ")*>
by GROUP_1:def 4
;
then ((((incl2 (G,A,phi)) . a) ") * ((incl1 (G,A,phi)) . g)) * ((incl2 (G,A,phi)) . a) =
<*((phi1 . g) * (phi1 . (1_ G))),((a ") * a)*>
by A1, Th14
.=
<*((phi1 . g) * (1_ G)),((a ") * a)*>
by GROUP_6:31
.=
<*(phi1 . g),((a ") * a)*>
by GROUP_1:def 4
.=
<*(phi1 . g),(1_ A)*>
by GROUP_1:def 5
;
hence
((incl1 (G,A,phi)) . g) |^ ((incl2 (G,A,phi)) . a) = <*((phi . (a ")) . g),(1_ A)*>
by GROUP_3:def 2; verum