defpred S1[ set , set , set ] means ( ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & $2 = [A9,d9] & $3 = [Aq,dq] ) or ( $3 = 0 & ( for A9 being non empty set
for d9 being distance_function of A9,L
for Aq being non empty set
for dq being distance_function of Aq,L holds
( not Aq,dq is_extension2_of A9,d9 or not $2 = [A9,d9] ) ) ) );
A1: for n being Nat
for x being set ex y being set st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[n,x,y]
per cases ( ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & x = [A9,d9] ) or for A9 being non empty set
for d9 being distance_function of A9,L
for Aq being non empty set
for dq being distance_function of Aq,L holds
( not Aq,dq is_extension2_of A9,d9 or not x = [A9,d9] ) ) ;
suppose ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & x = [A9,d9] ) ; :: thesis: ex y being set st S1[n,x,y]
then consider A9 being non empty set , d9 being distance_function of A9,L, Aq being non empty set , dq being distance_function of Aq,L such that
A2: ( Aq,dq is_extension2_of A9,d9 & x = [A9,d9] ) ;
take [Aq,dq] ; :: thesis: ( [Aq,dq] is set & S1[n,x,[Aq,dq]] )
thus ( [Aq,dq] is set & S1[n,x,[Aq,dq]] ) by A2; :: thesis: verum
end;
suppose A3: for A9 being non empty set
for d9 being distance_function of A9,L
for Aq being non empty set
for dq being distance_function of Aq,L holds
( not Aq,dq is_extension2_of A9,d9 or not x = [A9,d9] ) ; :: thesis: ex y being set st S1[n,x,y]
take 0 ; :: thesis: S1[n,x, 0 ]
thus S1[n,x, 0 ] by A3; :: thesis: verum
end;
end;
end;
consider f being Function such that
A4: dom f = NAT and
A5: f . 0 = [A,d] and
A6: for n being Nat holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A1);
 take f ; :: thesis: ( dom f = NAT & f . 0 = [A,d] & ( for n being Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & f . n = [A9,d9] & f . (n + 1) = [Aq,dq] ) ) )
thus dom f = NAT by A4; :: thesis: ( f . 0 = [A,d] & ( for n being Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & f . n = [A9,d9] & f . (n + 1) = [Aq,dq] ) ) )
thus f . 0 = [A,d] by A5; :: thesis: for n being Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & f . n = [A9,d9] & f . (n + 1) = [Aq,dq] )
defpred S2[ Nat] means ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & f . $1 = [A9,d9] & f . ($1 + 1) = [Aq,dq] );
A7: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
given A9 being non empty set , d9 being distance_function of A9,L, Aq being non empty set , dq being distance_function of Aq,L such that Aq,dq is_extension2_of A9,d9 and
f . k = [A9,d9] and
A8: f . (k + 1) = [Aq,dq] ; :: thesis: S2[k + 1]
ex A1 being non empty set ex d1 being distance_function of A1,L ex AQ being non empty set ex DQ being distance_function of AQ,L st
( AQ,DQ is_extension2_of A1,d1 & f . (k + 1) = [A1,d1] )
proof
set Q = the QuadrSeq of dq;
set AQ = NextSet2 dq;
take Aq ; :: thesis: ex d1 being distance_function of Aq,L ex AQ being non empty set ex DQ being distance_function of AQ,L st
( AQ,DQ is_extension2_of Aq,d1 & f . (k + 1) = [Aq,d1] )
take dq ; :: thesis: ex AQ being non empty set ex DQ being distance_function of AQ,L st
( AQ,DQ is_extension2_of Aq,dq & f . (k + 1) = [Aq,dq] )
set DQ = NextDelta2 the QuadrSeq of dq;
take NextSet2 dq ; :: thesis: ex DQ being distance_function of (NextSet2 dq),L st
( NextSet2 dq,DQ is_extension2_of Aq,dq & f . (k + 1) = [Aq,dq] )
take NextDelta2 the QuadrSeq of dq ; :: thesis: ( NextSet2 dq, NextDelta2 the QuadrSeq of dq is_extension2_of Aq,dq & f . (k + 1) = [Aq,dq] )
thus NextSet2 dq, NextDelta2 the QuadrSeq of dq is_extension2_of Aq,dq ; :: thesis: f . (k + 1) = [Aq,dq]
thus f . (k + 1) = [Aq,dq] by A8; :: thesis: verum
end;
hence S2[k + 1] by A6; :: thesis: verum
end;
ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & f . 0 = [A9,d9] )
proof
set Aq = NextSet2 d;
set q = the QuadrSeq of d;
take A ; :: thesis: ex d9 being distance_function of A,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A,d9 & f . 0 = [A,d9] )
take d ; :: thesis: ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A,d & f . 0 = [A,d] )
consider dq being distance_function of (NextSet2 d),L such that
A9: dq = NextDelta2 the QuadrSeq of d ;
take NextSet2 d ; :: thesis: ex dq being distance_function of (NextSet2 d),L st
( NextSet2 d,dq is_extension2_of A,d & f . 0 = [A,d] )
take dq ; :: thesis: ( NextSet2 d,dq is_extension2_of A,d & f . 0 = [A,d] )
thus NextSet2 d,dq is_extension2_of A,d by A9; :: thesis: f . 0 = [A,d]
thus f . 0 = [A,d] by A5; :: thesis: verum
end;
then A10: S2[ 0 ] by A6;
thus for k being Nat holds S2[k] from NAT_1:sch 2(A10, A7); :: thesis: verum