take pr1 (A,A) ; :: thesis: pr1 (A,A) is idempotent

per cases ( A <> {} or A = {} ) ;

suppose A1: A <> {} ; :: thesis: pr1 (A,A) is idempotent

let a be Element of A; :: according to BINOP_1:def 4 :: thesis: (pr1 (A,A)) . (a,a) = a
a in A by A1;
hence (pr1 (A,A)) . (a,a) = a by Def4; :: thesis: verum

end;

suppose A2: A = {} ; :: thesis: pr1 (A,A) is idempotent

let a be Element of A; :: according to BINOP_1:def 4 :: thesis: (pr1 (A,A)) . (a,a) = a
not [a,a] in dom (pr1 (A,A)) by A2;
hence (pr1 (A,A)) . (a,a) = {} by FUNCT_1:def 2
.= a by A2, SUBSET_1:def 1 ;
:: thesis: verum

end;

end;