defpred S₁[ Function of (INT.Group 2),(AutGroup G)] means ( $1 . 0 = id G & $1 . 1 = inverse_op G );
let f1, f2 be Function of (INT.Group 2),(AutGroup G); :: thesis: ( f1 . 0 = id G & f1 . 1 = inverse_op G & f2 . 0 = id G & f2 . 1 = inverse_op G implies f1 = f2 )
assume A1: S₁[f1] ; :: thesis: ( not f2 . 0 = id G or not f2 . 1 = inverse_op G or f1 = f2 )
assume A2: S₁[f2] ; :: thesis: f1 = f2
for x being Element of (INT.Group 2) holds f1 . x = f2 . x

proof

let x be Element of (INT.Group 2); :: thesis: f1 . x = f2 . x
x in the carrier of (INT.Group 2) ;
then x in Segm 2 by Th76;
then ( x = 0 or x = 1 ) by CARD_1:50, TARSKI:def 2;
hence f1 . x = f2 . x by A1, A2; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:def 7; :: thesis: verum