let G, A be Group; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ((incl1 (G,A,phi)) . g) |^ ((incl2 (G,A,phi)) . (a ")) = <*((phi . a) . g),(1_ A)*>
thus ((incl1 (G,A,phi)) . g) |^ ((incl2 (G,A,phi)) . (a ")) = <*((phi . ((a ") ")) . g),(1_ A)*> by Th36
.= <*((phi . a) . g),(1_ A)*> ; :: thesis: verum