let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for a1, a2 being Element of A
for x, y, z being Element of (semidirect_product (G,A,phi)) st x = <*(1_ G),a1*> & y = <*(1_ G),a2*> & z = <*(1_ G),(a1 * a2)*> holds
x * y = z
let phi be Homomorphism of A,(AutGroup G); :: thesis: for a1, a2 being Element of A
for x, y, z being Element of (semidirect_product (G,A,phi)) st x = <*(1_ G),a1*> & y = <*(1_ G),a2*> & z = <*(1_ G),(a1 * a2)*> holds
x * y = z
let a1, a2 be Element of A; :: thesis: for x, y, z being Element of (semidirect_product (G,A,phi)) st x = <*(1_ G),a1*> & y = <*(1_ G),a2*> & z = <*(1_ G),(a1 * a2)*> holds
x * y = z
let x, y, z be Element of (semidirect_product (G,A,phi)); :: thesis: ( x = <*(1_ G),a1*> & y = <*(1_ G),a2*> & z = <*(1_ G),(a1 * a2)*> implies x * y = z )
assume A1: x = <*(1_ G),a1*> ; :: thesis: ( not y = <*(1_ G),a2*> or not z = <*(1_ G),(a1 * a2)*> or x * y = z )
assume A2: y = <*(1_ G),a2*> ; :: thesis: ( not z = <*(1_ G),(a1 * a2)*> or x * y = z )
assume A3: z = <*(1_ G),(a1 * a2)*> ; :: thesis: x * y = z
reconsider phi1 = phi . a1 as Homomorphism of G,G by AUTGROUP:def 1;
thus x * y = <*((1_ G) * (phi1 . (1_ G))),(a1 * a2)*> by A1, A2, Th14
.= <*((1_ G) * (1_ G)),(a1 * a2)*> by GROUP_6:31
.= z by A3, GROUP_1:def 4 ; :: thesis: verum