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;

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

let y be object ; :: thesis: ( y in (* h) .: P implies y in P * h )
assume y in (* h) .: P ; :: thesis: y in P * h
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 = x * h by Def2;
hence y in P * h by A2, GROUP_2:28; :: thesis: verum

end;

let y be object ; :: 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:28;
( dom (* h) = the carrier of H & (* h) . s = s * h ) by Def2, FUNCT_2:def 1;
hence y in (* h) .: P by A3, FUNCT_1:def 6; :: thesis: verum