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

proof

let x be Element of A; :: thesis: ex y being Element of (semidirect_product (G,A,phi)) st S₁[x,y]
reconsider y = <*(1_ G),x*> 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 A,(semidirect_product (G,A,phi)) such that
A2: for x being Element of A holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for a being Element of A holds f . a = <*(1_ G),a*>
thus for a being Element of A holds f . a = <*(1_ G),a*> by A2; :: thesis: verum