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 a1, a2 being Element of A
for g1, g2, g3 being Element of G st x = <*g1,a1*> & y = <*g2,a2*> & g3 = (phi . a1) . g2 holds
x * y = <*(g1 * g3),(a1 * a2)*>
let phi be Homomorphism of A,(AutGroup G); :: thesis: for x, y being Element of (semidirect_product (G,A,phi))
for a1, a2 being Element of A
for g1, g2, g3 being Element of G st x = <*g1,a1*> & y = <*g2,a2*> & g3 = (phi . a1) . g2 holds
x * y = <*(g1 * g3),(a1 * a2)*>
let x, y be Element of (semidirect_product (G,A,phi)); :: thesis: for a1, a2 being Element of A
for g1, g2, g3 being Element of G st x = <*g1,a1*> & y = <*g2,a2*> & g3 = (phi . a1) . g2 holds
x * y = <*(g1 * g3),(a1 * a2)*>
let a1, a2 be Element of A; :: thesis: for g1, g2, g3 being Element of G st x = <*g1,a1*> & y = <*g2,a2*> & g3 = (phi . a1) . g2 holds
x * y = <*(g1 * g3),(a1 * a2)*>
let g1, g2, g3 be Element of G; :: thesis: ( x = <*g1,a1*> & y = <*g2,a2*> & g3 = (phi . a1) . g2 implies x * y = <*(g1 * g3),(a1 * a2)*> )
assume A1: x = <*g1,a1*> ; :: thesis: ( not y = <*g2,a2*> or not g3 = (phi . a1) . g2 or x * y = <*(g1 * g3),(a1 * a2)*> )
assume A2: y = <*g2,a2*> ; :: thesis: ( not g3 = (phi . a1) . g2 or x * y = <*(g1 * g3),(a1 * a2)*> )
assume A3: g3 = (phi . a1) . g2 ; :: thesis: x * y = <*(g1 * g3),(a1 * a2)*>
( x in product (Carrier <*G,A*>) & y in product (Carrier <*G,A*>) )

proof

x in semidirect_product (G,A,phi) ;
hence x in product (Carrier <*G,A*>) by Def1; :: thesis: y in product (Carrier <*G,A*>)
y in semidirect_product (G,A,phi) ;
hence y in product (Carrier <*G,A*>) by Def1; :: thesis: verum

end;

then consider h being Function, aa1 being Element of A, gg2 being Element of G such that
A4: ( h = x * y & aa1 = x . 2 & gg2 = y . 1 & h . 1 = the multF of G . ((x . 1),((phi . aa1) . gg2)) & h . 2 = the multF of A . ((x . 2),(y . 2)) ) by Def1;
A5: ( a1 = aa1 & g2 = gg2 ) by A1, A2, A4;
A6: h . 2 = the multF of A . ((x . 2),a2) by A2, A4
.= the multF of A . (a1,a2) by A1 ;
A7: (x * y) . 1 = g1 * g3 by A1, A3, A4, A5;
dom (x * y) = {1,2} by Th11;
then len (x * y) = 2 by FINSEQ_1:2, FINSEQ_1:def 3;
hence x * y = <*(g1 * g3),(a1 * a2)*> by A4, A6, A7, FINSEQ_1:44; :: thesis: verum