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