set I = id A;
thus {(id A)} is composition-closed :: thesis: {(id A)} is inverse-closed
proof
let f, g be Element of {(id A)}; :: according to AIMLOOP:def 36 :: thesis: ( f in {(id A)} & g in {(id A)} implies f * g in {(id A)} )
( f = id A & g = id A ) by TARSKI:def 1;
hence ( f in {(id A)} & g in {(id A)} implies f * g in {(id A)} ) by SYSREL:12; :: thesis: verum
end;
let f be Element of {(id A)}; :: according to AIMLOOP:def 37 :: thesis: ( f in {(id A)} implies f " in {(id A)} )
f = id A by TARSKI:def 1;
then ( f is Permutation of A & (id A) * f = id A ) by SYSREL:12;
then f " = id A by FUNCT_2:60;
hence ( f in {(id A)} implies f " in {(id A)} ) by TARSKI:def 1; :: thesis: verum