defpred S₂[ set , set ] means $2 = [\((rfs r) . $1)/];
A1: for x being Element of NAT ex y being Element of INT st S₂[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of INT st S₂[x,y]
reconsider y = [\((rfs r) . x)/] as Element of INT by INT_1:def 2;
take y ; :: thesis: S₂[x,y]
thus S₂[x,y] ; :: thesis: verum

end;

consider f being sequence of INT such that
A2: for x being Element of NAT holds S₂[x,f . x] from FUNCT_2:sch 3(A1);
reconsider f = f as Integer_Sequence by Th9;
take f ; :: thesis: for n being Nat holds f . n = [\((rfs r) . n)/]
let n be Nat; :: thesis: f . n = [\((rfs r) . n)/]
n in NAT by ORDINAL1:def 12;
hence f . n = [\((rfs r) . n)/] by A2; :: thesis: verum