set n2 = 2 + n;
set F = (2 + n) |^ f;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom ((2 + n) |^ f) or not x2 in dom ((2 + n) |^ f) or not ((2 + n) |^ f) . x1 = ((2 + n) |^ f) . x2 or x1 = x2 )
assume A1: ( x1 in dom ((2 + n) |^ f) & x2 in dom ((2 + n) |^ f) & ((2 + n) |^ f) . x1 = ((2 + n) |^ f) . x2 ) ; :: thesis: x1 = x2
A2: dom ((2 + n) |^ f) = dom f by Def4;
then A3: ( ((2 + n) |^ f) . x1 = (2 + n) to_power (f . x1) & ((2 + n) |^ f) . x2 = (2 + n) to_power (f . x2) ) by A1, Def4;
(n + 1) + 1 > 0 + 1 by XREAL_1:8;
then f . x1 = f . x2 by A1, A3, PEPIN:30;
hence x1 = x2 by A1, A2, FUNCT_1:def 4; :: thesis: verum