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

proof

let e be set ; :: thesis: ( e in { (m + k) where m is Element of NAT : m in dom p } implies ex u being set st S₁[e,u] )
assume e in { (m + k) where m is Element of NAT : m in dom p } ; :: thesis: ex u being set st S₁[e,u]
then consider m being Element of NAT such that
A2: ( e = m + k & 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 Element of NAT : m in dom p } and
A4: for e being set st e in { (m + k) where m is Element of 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 Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
f . (m + k) = p . m ) )
thus dom f = { (m + k) where m is Element of NAT : m in dom p } by A3; :: thesis: for m being Element of NAT st m in dom p holds
f . (m + k) = p . m
let m be Element of 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 Element of NAT : m in dom p } ;
then consider j being Element of NAT such that
A25: m + k = j + k and
A26: f . (m + k) = p . j by A4;
thus f . (m + k) = p . m by A25, A26; :: thesis: verum