let r1, r2 be Real; :: thesis: for k being Nat
for seq1 being Real_Sequence ex seq being Real_Sequence st
( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )
let k be Nat; :: thesis: for seq1 being Real_Sequence ex seq being Real_Sequence st
( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )
let seq1 be Real_Sequence; :: thesis: ex seq being Real_Sequence st
( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )
ex seq being Real_Sequence st
for n being Nat holds
( ( n = 0 implies seq . n = r1 ) & ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n <> 0 & n > k implies seq . n = r2 ) )

proof

defpred S₁[ object , object ] means ex n being Nat st
( n = $1 & ( n = 0 implies $2 = r1 ) & ( n <> 0 & n <= k implies $2 = seq1 . n ) & ( n <> 0 & n > k implies $2 = r2 ) );
A1: for x being object st x in NAT holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st S₁[x,y] )
assume x in NAT ; :: thesis: ex y being object st S₁[x,y]
then reconsider n = x as Nat ;

now :: thesis: ( ( n = 0 & S₁[x,r1] ) or ( n <> 0 & n <= k & S₁[x,seq1 . n] ) or ( n <> 0 & not n <= k & S₁[x,r2] ) )

per cases ( n = 0 or ( n <> 0 & n <= k ) or ( n <> 0 & not n <= k ) ) ;

case n = 0 ; :: thesis: S₁[x,r1]

hence S₁[x,r1] ; :: thesis: verum

end;

case ( n <> 0 & n <= k ) ; :: thesis: S₁[x,seq1 . n]

hence S₁[x,seq1 . n] ; :: thesis: verum

end;

case ( n <> 0 & not n <= k ) ; :: thesis: S₁[x,r2]

hence S₁[x,r2] ; :: thesis: verum

end;

end;

end;

hence ex y being object st S₁[x,y] ; :: thesis: verum

end;

consider f1 being Function such that
A2: ( dom f1 = NAT & ( for x being object st x in NAT holds
S₁[x,f1 . x] ) ) from CLASSES1:sch 1(A1);

now :: thesis: for x being object st x in NAT holds
f1 . x is real

let x be object ; :: thesis: ( x in NAT implies f1 . x is real )
assume x in NAT ; :: thesis: f1 . x is real
then ex n being Nat st
( n = x & ( n = 0 implies f1 . x = r1 ) & ( n <> 0 & n <= k implies f1 . x = seq1 . n ) & ( n <> 0 & n > k implies f1 . x = r2 ) ) by A2;
hence f1 . x is real ; :: thesis: verum

end;

then reconsider f1 = f1 as Real_Sequence by A2, SEQ_1:1;
take seq = f1; :: thesis: for n being Nat holds
( ( n = 0 implies seq . n = r1 ) & ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n <> 0 & n > k implies seq . n = r2 ) )
let n be Nat; :: thesis: ( ( n = 0 implies seq . n = r1 ) & ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n <> 0 & n > k implies seq . n = r2 ) )
reconsider n = n as Element of NAT by ORDINAL1:def 12;
ex k1 being Nat st
( k1 = n & ( k1 = 0 implies seq . n = r1 ) & ( k1 <> 0 & k1 <= k implies seq . n = seq1 . k1 ) & ( k1 <> 0 & k1 > k implies seq . n = r2 ) ) by A2;
hence ( ( n = 0 implies seq . n = r1 ) & ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n <> 0 & n > k implies seq . n = r2 ) ) ; :: thesis: verum

end;

then consider seq being Real_Sequence such that
A3: for n being Nat holds
( ( n = 0 implies seq . n = r1 ) & ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n <> 0 & n > k implies seq . n = r2 ) ) ;
take seq ; :: thesis: ( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )
thus ( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) ) by A3; :: thesis: verum