:: by Marco Riccardi

::

:: Received August 13, 2007

:: Copyright (c) 2007-2018 Association of Mizar Users

notation

let S be non empty 1-sorted ;

let E be set ;

let A be Action of the carrier of S,E;

let s be Element of S;

synonym A ^ s for S . E;

end;
let E be set ;

let A be Action of the carrier of S,E;

let s be Element of S;

synonym A ^ s for S . E;

definition

let S be non empty 1-sorted ;

let E be set ;

let A be Action of the carrier of S,E;

let s be Element of S;

:: original: ^

redefine func A ^ s -> Function of E,E;

correctness

coherence

^ is Function of E,E;

end;
let E be set ;

let A be Action of the carrier of S,E;

let s be Element of S;

:: original: ^

redefine func A ^ s -> Function of E,E;

correctness

coherence

^ is Function of E,E;

proof end;

definition
end;

:: deftheorem Def1 defines being_left_operation GROUP_10:def 1 :

for S being non empty unital multMagma

for E being set

for A being Action of the carrier of S,E holds

( A is being_left_operation iff ( A ^ (1_ S) = id E & ( for s1, s2 being Element of S holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) ) );

for S being non empty unital multMagma

for E being set

for A being Action of the carrier of S,E holds

( A is being_left_operation iff ( A ^ (1_ S) = id E & ( for s1, s2 being Element of S holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) ) );

registration

let S be non empty unital multMagma ;

let E be set ;

existence

ex b_{1} being Action of the carrier of S,E st b_{1} is being_left_operation ;

end;
let E be set ;

cluster Relation-like the carrier of S -defined Funcs (E,E) -valued non empty Function-like total quasi_total being_left_operation for Action of ,;

correctness existence

ex b

proof end;

:: ALG I.5.1 DEF 1

definition

let S be non empty unital multMagma ;

let E be set ;

mode LeftOperation of S,E is being_left_operation Action of the carrier of S,E;

end;
let E be set ;

mode LeftOperation of S,E is being_left_operation Action of the carrier of S,E;

scheme :: GROUP_10:sch 1

ExLeftOperation{ F_{1}() -> set , F_{2}() -> non empty Group-like multMagma , F_{3}( Element of F_{2}()) -> Function of F_{1}(),F_{1}() } :

ExLeftOperation{ F

ex T being LeftOperation of F_{2}(),F_{1}() st

for s being Element of F_{2}() holds T . s = F_{3}(s)

providedfor s being Element of F