defpred S₁[ object , object ] means ex m being Nat st
( $1 = m + k & $2 = p . m );
set A = { (m + k) where m is Nat : m in dom p } ;
A1: for e being object st e in { (m + k) where m is Nat : m in dom p } holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in { (m + k) where m is Nat : m in dom p } implies ex u being object st S₁[e,u] )
assume e in { (m + k) where m is Nat : m in dom p } ; :: thesis: ex u being object st S₁[e,u]
then consider m being Nat such that
A2: e = m + k and
m in dom p ;
take p . m ; :: thesis: S₁[e,p . m]
thus S₁[e,p . m] by A2; :: thesis: verum

end;

consider f being Function such that
A3: dom f = { (m + k) where m is Nat : m in dom p } and
A4: for e being object st e in { (m + k) where m is Nat : m in dom p } holds
S₁[e,f . e] from CLASSES1:sch 1(A1);
take f ; :: thesis: ( dom f = { (m + k) where m is Nat : m in dom p } & ( for m being Nat st m in dom p holds
f . (m + k) = p . m ) )
thus dom f = { (m + k) where m is Nat : m in dom p } by A3; :: thesis: for m being Nat st m in dom p holds
f . (m + k) = p . m
let m be Nat; :: thesis: ( m in dom p implies f . (m + k) = p . m )
assume m in dom p ; :: thesis: f . (m + k) = p . m
then m + k in { (m + k) where m is Nat : m in dom p } ;
then ex j being Nat st
( m + k = j + k & f . (m + k) = p . j ) by A4;
hence f . (m + k) = p . m ; :: thesis: verum