defpred S₁[ Element of (INT.Group 2), Element of (AutGroup G)] means ( ( 0 = $1 implies $2 = id G ) & ( 1 = $1 implies $2 = inverse_op G ) );
A1: for x being Element of (INT.Group 2) ex y being Element of (AutGroup G) st S₁[x,y]

proof

let x be Element of (INT.Group 2); :: thesis: ex y being Element of (AutGroup G) st S₁[x,y]
x in INT.Group 2 ;
then x in Segm 2 by Th76;

per cases then ( x = 0 or x = 1 ) by CARD_1:50, TARSKI:def 2;

suppose B1: x = 0 ; :: thesis: ex y being Element of (AutGroup G) st S₁[x,y]

reconsider y = id G as Element of (AutGroup G) by AUTGROUP:3;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by B1; :: thesis: verum

end;

suppose B2: x = 1 ; :: thesis: ex y being Element of (AutGroup G) st S₁[x,y]

reconsider y = inverse_op G as Element of (AutGroup G) by GROUP_22:25;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by B2; :: thesis: verum

end;

end;

end;

consider f being Function of (INT.Group 2),(AutGroup G) such that
A2: for x being Element of (INT.Group 2) holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: ( f . 0 = id G & f . 1 = inverse_op G )
0 in INT.Group 2 by EltsOfINTGroup2;
hence f . 0 = id G by A2; :: thesis: f . 1 = inverse_op G
2 = 2 * 1 ;
then 1 in Segm 2 by Lm6;
then 1 in the carrier of (INT.Group 2) by Th76;
hence f . 1 = inverse_op G by A2; :: thesis: verum