let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for x, y being Element of (semidirect_product (G,A,phi))
for a being Element of A
for g being Element of G st x = <*g,(1_ A)*> & y = <*(1_ G),a*> holds
x * y = <*g,a*>
let phi be Homomorphism of A,(AutGroup G); :: thesis: for x, y being Element of (semidirect_product (G,A,phi))
for a being Element of A
for g being Element of G st x = <*g,(1_ A)*> & y = <*(1_ G),a*> holds
x * y = <*g,a*>
let x, y be Element of (semidirect_product (G,A,phi)); :: thesis: for a being Element of A
for g being Element of G st x = <*g,(1_ A)*> & y = <*(1_ G),a*> holds
x * y = <*g,a*>
let a be Element of A; :: thesis: for g being Element of G st x = <*g,(1_ A)*> & y = <*(1_ G),a*> holds
x * y = <*g,a*>
let g be Element of G; :: thesis: ( x = <*g,(1_ A)*> & y = <*(1_ G),a*> implies x * y = <*g,a*> )
assume A1: x = <*g,(1_ A)*> ; :: thesis: ( not y = <*(1_ G),a*> or x * y = <*g,a*> )
assume A2: y = <*(1_ G),a*> ; :: thesis: x * y = <*g,a*>
(phi . (1_ A)) . (1_ G) = 1_ G by Th15;
hence x * y = <*(g * (1_ G)),((1_ A) * a)*> by A1, A2, Th14
.= <*g,((1_ A) * a)*> by GROUP_1:def 4
.= <*g,a*> by GROUP_1:def 4 ;
:: thesis: verum