defpred S₁[ Nat, set , set ] means $3 = R_NormSpace_of_BoundedLinearOperators (S,(modetrans $2));
A1: for n being Nat
for x being set ex y being set st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being set ex y being set st S₁[n,x,y]
let x be set ; :: thesis: ex y being set st S₁[n,x,y]
take y = R_NormSpace_of_BoundedLinearOperators (S,(modetrans x)); :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: verum

end;

thus ex g being Function st
( dom g = NAT & g . 0 = T & ( for n being Nat holds S₁[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch 1(A1); :: thesis: verum