defpred S₁[ Element of G, Element of (semidirect_product (G,A,phi))] means $2 = <*$1,(1_ A)*>;
A1: for x being Element of G ex y being Element of (semidirect_product (G,A,phi)) st S₁[x,y]

proof

let x be Element of G; :: thesis: ex y being Element of (semidirect_product (G,A,phi)) st S₁[x,y]
reconsider y = <*x,(1_ A)*> as Element of (semidirect_product (G,A,phi)) by Th9;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function of G,(semidirect_product (G,A,phi)) such that
A2: for x being Element of G holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for g being Element of G holds f . g = <*g,(1_ A)*>
thus for g being Element of G holds f . g = <*g,(1_ A)*> by A2; :: thesis: verum