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₁[ set , set ] means ex n being Element of 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 set st x in NAT holds
ex y being set st S₁[x,y]

proof

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

now

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 set st S₁[x,y] ; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( x in NAT implies f1 . x is real )
assume x in NAT ; :: thesis: f1 . x is real
then ex n being Element of 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 A3;
hence f1 . x is real ; :: thesis: verum

end;

then reconsider f1 = f1 as Real_Sequence by A3, SEQ_1:3;
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 13;
ex k1 being Element of 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 A3;
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
A4: 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 A4; :: thesis: verum