defpred S1[ set , set , set ] means ( ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A',d' & $2 = [A',d'] & $3 = [Aq,dq] ) or ( $3 = 0 & ( for A' being non empty set
for d' being distance_function of A',L
for Aq being non empty set
for dq being distance_function of Aq,L holds
( not Aq,dq is_extension_of A',d' or not $2 = [A',d'] ) ) ) );
A1:
for n being Element of NAT
for x being set ex y being set st S1[n,x,y]
proof
let n be
Element of
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 A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A',d' & x = [A',d'] ) or for A' being non empty set
for d' being distance_function of A',L
for Aq being non empty set
for dq being distance_function of Aq,L holds
( not Aq,dq is_extension_of A',d' or not x = [A',d'] ) )
;
suppose
ex
A' being non
empty set ex
d' being
distance_function of
A',
L ex
Aq being non
empty set ex
dq being
distance_function of
Aq,
L st
(
Aq,
dq is_extension_of A',
d' &
x = [A',d'] )
;
:: thesis: ex y being set st S1[n,x,y]then consider A' being non
empty set ,
d' being
distance_function of
A',
L,
Aq being non
empty set ,
dq being
distance_function of
Aq,
L such that A2:
Aq,
dq is_extension_of A',
d'
and A3:
x = [A',d']
;
take
[Aq,dq]
;
:: thesis: S1[n,x,[Aq,dq]]thus
S1[
n,
x,
[Aq,dq]]
by A2, A3;
:: thesis: verum end;
end;
consider f being Function such that
A5:
dom f = NAT
and
A6:
f . 0 = [A,d]
and
A7:
for n being Element of 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 Element of NAT ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A',d' & f . n = [A',d'] & f . (n + 1) = [Aq,dq] ) ) )
thus
dom f = NAT
by A5; :: thesis: ( f . 0 = [A,d] & ( for n being Element of NAT ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A',d' & f . n = [A',d'] & f . (n + 1) = [Aq,dq] ) ) )
thus
f . 0 = [A,d]
by A6; :: thesis: for n being Element of NAT ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A',d' & f . n = [A',d'] & f . (n + 1) = [Aq,dq] )
defpred S2[ Element of NAT ] means ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A',d' & f . $1 = [A',d'] & f . ($1 + 1) = [Aq,dq] );
ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A',d' & f . 0 = [A',d'] )
proof
take
A
;
:: thesis: ex d' being distance_function of A,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A,d' & f . 0 = [A,d'] )
take
d
;
:: thesis: ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A,d & f . 0 = [A,d] )
consider q being
QuadrSeq of
d;
set Aq =
NextSet d;
consider dq being
distance_function of
(NextSet d),
L such that A8:
dq = NextDelta q
;
take
NextSet d
;
:: thesis: ex dq being distance_function of (NextSet d),L st
( NextSet d,dq is_extension_of A,d & f . 0 = [A,d] )
take
dq
;
:: thesis: ( NextSet d,dq is_extension_of A,d & f . 0 = [A,d] )
thus
NextSet d,
dq is_extension_of A,
d
by A8, Def20;
:: thesis: f . 0 = [A,d]
thus
f . 0 = [A,d]
by A6;
:: thesis: verum
end;
then A9:
S2[ 0 ]
by A7;
A10:
for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S2[k] implies S2[k + 1] )
given A' being non
empty set ,
d' being
distance_function of
A',
L,
Aq being non
empty set ,
dq being
distance_function of
Aq,
L such that
Aq,
dq is_extension_of A',
d'
and
f . k = [A',d']
and A11:
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_extension_of A1,
d1 &
f . (k + 1) = [A1,d1] )
proof
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_extension_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_extension_of Aq,dq & f . (k + 1) = [Aq,dq] )
set AQ =
NextSet dq;
consider Q being
QuadrSeq of
dq;
set DQ =
NextDelta Q;
take
NextSet dq
;
:: thesis: ex DQ being distance_function of (NextSet dq),L st
( NextSet dq,DQ is_extension_of Aq,dq & f . (k + 1) = [Aq,dq] )
take
NextDelta Q
;
:: thesis: ( NextSet dq, NextDelta Q is_extension_of Aq,dq & f . (k + 1) = [Aq,dq] )
thus
NextSet dq,
NextDelta Q is_extension_of Aq,
dq
by Def20;
:: thesis: f . (k + 1) = [Aq,dq]
thus
f . (k + 1) = [Aq,dq]
by A11;
:: thesis: verum
end;
hence
S2[
k + 1]
by A7;
:: thesis: verum
end;
thus
for k being Element of NAT holds S2[k]
from NAT_1:sch 1(A9, A10); :: thesis: verum