defpred S1[ 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 S1[n,x,y]
proof
let n be
Nat;
for x being Subset of REAL ex y being Subset of REAL st S1[n,x,y]let x be
Subset of
REAL;
ex y being Subset of REAL st S1[n,x,y]
take
x \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1))
;
S1[n,x,x \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1))]
thus
S1[
n,
x,
x \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1))]
;
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 S1[n,F . n,F . (n + 1)]
from RECDEF_1:sch 2(A1);
take
F
; ( 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; for n being Nat holds F . (n + 1) = (F . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1))
let n be Nat; 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; verum