defpred S₁[ set , set , set ] means for x, y being Subset of REAL
for s being Nat st s = $1 & x = $2 & y = $3 holds
y = x \/ ((GoCross_Seq_REAL (pm,k)) . (s + 1));
A1: for n being Nat
for x being Subset of REAL ex y being Subset of REAL st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Subset of REAL ex y being Subset of REAL st S₁[n,x,y]
let x be Subset of REAL; :: thesis: ex y being Subset of REAL st S₁[n,x,y]
take x \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ; :: thesis: S₁[n,x,x \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1))]
thus S₁[n,x,x \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1))] ; :: thesis: verum

end;

consider F being SetSequence of REAL such that
A2: F . 0 = (GoCross_Seq_REAL (pm,k)) . 0 and
A3: for n being Nat holds S₁[n,F . n,F . (n + 1)] from RECDEF_1:sch 2(A1);
take F ; :: thesis: ( F . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds F . (n + 1) = (F . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) )
thus F . 0 = (GoCross_Seq_REAL (pm,k)) . 0 by A2; :: thesis: for n being Nat holds F . (n + 1) = (F . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1))
let n be Nat; :: thesis: F . (n + 1) = (F . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1))
thus F . (n + 1) = (F . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) by A3; :: thesis: verum