reconsider IT = [: the carrier of S,{(id E)}:] as Action of the carrier of S,E by GROUP_9:62;
take IT ; :: thesis: IT is being_left_operation

A1: now :: thesis: for s being Element of S holds IT . s = id E

let s be Element of S; :: thesis: IT . s = id E
IT c= [: the carrier of S,{(id E)}:] ;
then reconsider IT9 = IT as Relation of the carrier of S,{(id E)} ;

now :: thesis: for x being object st x in the carrier of S holds
ex y being object st [x,y] in [: the carrier of S,{(id E)}:]

let x be object ; :: thesis: ( x in the carrier of S implies ex y being object st [x,y] in [: the carrier of S,{(id E)}:] )
assume A2: x in the carrier of S ; :: thesis: ex y being object st [x,y] in [: the carrier of S,{(id E)}:]
reconsider y = id E as object ;
take y = y; :: thesis: [x,y] in [: the carrier of S,{(id E)}:]
y in {(id E)} by TARSKI:def 1;
hence [x,y] in [: the carrier of S,{(id E)}:] by A2, ZFMISC_1:def 2; :: thesis: verum

end;

then dom IT9 = the carrier of S by RELSET_1:9;
then A3: IT . s in rng IT by FUNCT_1:3;
rng IT9 c= {(id E)} ;
hence IT . s = id E by A3, TARSKI:def 1; :: thesis: verum

end;

hence IT ^ (1_ S) = id E ; :: according to GROUP_10:def 1 :: thesis: for s1, s2 being Element of S holds IT ^ (s1 * s2) = (IT ^ s1) * (IT ^ s2)
let s1, s2 be Element of S; :: thesis: IT ^ (s1 * s2) = (IT ^ s1) * (IT ^ s2)
( IT ^ s1 = id E & IT ^ s2 = id E ) by A1;
then (IT ^ s1) * (IT ^ s2) = id E by PARTFUN1:6;
hence IT ^ (s1 * s2) = (IT ^ s1) * (IT ^ s2) by A1; :: thesis: verum