let H be non empty multMagma ; :: thesis: for P being Subset of H
for h being Element of H holds (* h) .: P = P * h
let P be Subset of H; :: thesis: for h being Element of H holds (* h) .: P = P * h
let h be Element of H; :: thesis: (* h) .: P = P * h
set f = * h;
A1: dom (* h) = the carrier of H by FUNCT_2:def 1;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: P * h c= (* h) .: P

let y be set ; :: thesis: ( y in (* h) .: P implies y in P * h )
assume y in (* h) .: P ; :: thesis: y in P * h
then consider x being set such that
A2: ( x in dom (* h) & x in P & y = (* h) . x ) by FUNCT_1:def 12;
reconsider x = x as Element of H by A2;
(* h) . x = x * h by Def2;
hence y in P * h by A2, GROUP_2:34; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in P * h or y in (* h) .: P )
assume y in P * h ; :: thesis: y in (* h) .: P
then consider s being Element of H such that
A3: ( y = s * h & s in P ) by GROUP_2:34;
(* h) . s = s * h by Def2;
hence y in (* h) .: P by A1, A3, FUNCT_1:def 12; :: thesis: verum