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