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 set ; :: thesis: ( y in (h * ) .: P implies y in h * P )
assume y in (h * ) .: P ; :: thesis: y in h * P
then consider x being set such that
A1: x in dom (h * ) and
A2: ( x in P & y = (h * ) . x ) by FUNCT_1:def 12;
reconsider x = x as Element of H by A1;
(h * ) . x = h * x by Def1;
hence y in h * P by A2, GROUP_2:33; :: thesis: verum

end;

let y be set ; :: 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:33;
( 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 12; :: thesis: verum