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 let s be
Element of
S;
:: thesis: IT . s = id Enow let x be
set ;
:: thesis: ( x in the carrier of S implies ex y being set st [x,y] in [:the carrier of S,{(id E)}:] )assume A2:
x in the
carrier of
S
;
:: thesis: ex y being set st [x,y] in [:the carrier of S,{(id E)}:]consider y being
set such that A3:
y = id E
;
take y =
y;
:: thesis: [x,y] in [:the carrier of S,{(id E)}:]
y in {(id E)}
by A3, TARSKI:def 1;
hence
[x,y] in [:the carrier of S,{(id E)}:]
by A2, ZFMISC_1:def 2;
:: thesis: verum end; then
dom IT = the
carrier of
S
by RELSET_1:22;
then A4:
IT . s in rng IT
by FUNCT_1:12;
IT c= [:the carrier of S,{(id E)}:]
;
then reconsider IT' =
IT as
Relation of the
carrier of
S,
{(id E)} ;
rng IT' c= {(id E)}
;
hence
IT . s = id E
by A4, 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:36;
hence
IT ^ (s1 * s2) = (IT ^ s1) * (IT ^ s2)
by A1; :: thesis: verum