let H be non empty multMagma ; :: thesis: for P being Subset of H
for h being Element of H holds (h *) .: P = h * P
let P be Subset of H; :: thesis: for h being Element of H holds (h *) .: P = h * P
let h be Element of H; :: thesis: (h *) .: P = h * P
set f = h * ;

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

let y be object ; :: thesis: ( y in (h *) .: P implies y in h * P )
assume y in (h *) .: P ; :: thesis: y in h * P
then consider x being object such that
A1: x in dom (h *) and
A2: ( x in P & y = (h *) . x ) by FUNCT_1:def 6;
reconsider x = x as Element of H by A1;
(h *) . x = h * x by Def1;
hence y in h * P by A2, GROUP_2:27; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in h * P or y in (h *) .: P )
assume y in h * P ; :: thesis: y in (h *) .: P
then consider s being Element of H such that
A3: ( y = h * s & s in P ) by GROUP_2:27;
( dom (h *) = the carrier of H & (h *) . s = h * s ) by Def1, FUNCT_2:def 1;
hence y in (h *) .: P by A3, FUNCT_1:def 6; :: thesis: verum