let H be non empty addMagma ; :: 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, Th27; :: 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 Th27;
( 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