let f be ConwayGameChain; :: thesis: for n, m being Element of dom f st n < m holds
ConwayRank (f . n) in ConwayRank (f . m)
let n, m be Element of dom f; :: thesis: ( n < m implies ConwayRank (f . n) in ConwayRank (f . m) )
assume A1: n < m ; :: thesis: ConwayRank (f . n) in ConwayRank (f . m)
consider l being Nat such that
A2: dom f = Seg l by FINSEQ_1:def 2;
defpred S2[ Nat] means ( m - $1 in dom f implies ConwayRank (f . (m - $1)) in ConwayRank (f . m) );
n >= 1 by A2, FINSEQ_1:1;
then A3: m > 1 by A1, XXREAL_0:2;
A4: S2[1]
proof
assume m - 1 in dom f ; :: thesis: ConwayRank (f . (m - 1)) in ConwayRank (f . m)
then reconsider m1 = m - 1 as Element of dom f ;
f . m1 in the_Options_of (f . m) by A3, Def11;
hence ConwayRank (f . (m - 1)) in ConwayRank (f . m) by Th14; :: thesis: verum
end;
A5: for k being non zero Nat st S2[k] holds
S2[k + 1]
proof
let k be non zero Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A6: S2[k] ; :: thesis: S2[k + 1]
assume m - (k + 1) in dom f ; :: thesis: ConwayRank (f . (m - (k + 1))) in ConwayRank (f . m)
then reconsider mk1 = m - (k + 1) as Element of dom f ;
k <= k + 1 by XREAL_1:31;
then ( 1 <= mk1 & mk1 <= m - k & m - k <= m & m <= l ) by A2, FINSEQ_1:1, XREAL_1:10, XREAL_1:43;
then A7: ( 1 <= m - k & m - k <= l ) by XXREAL_0:2;
then ( m >= k + 1 & k <= k + 1 ) by XREAL_1:19, XREAL_1:31;
then m - k is Nat by NAT_1:21, XXREAL_0:2;
then reconsider mk = m - k as Element of dom f by A7, A2, FINSEQ_1:1;
A8: mk1 = mk - 1 ;
mk1 > 0 ;
then mk1 + 1 > 1 by XREAL_1:29;
then f . mk1 in the_Options_of (f . mk) by Def11, A8;
then ( ConwayRank (f . mk1) in ConwayRank (f . mk) & ConwayRank (f . mk) in ConwayRank (f . m) ) by Th14, A6;
hence ConwayRank (f . (m - (k + 1))) in ConwayRank (f . m) by ORDINAL1:10; :: thesis: verum
end;
A9: for k being non zero Nat holds S2[k] from NAT_1:sch 10(A4, A5);
 reconsider k = m - n as non zero Nat by A1, NAT_1:21;
m - k = n ;
hence ConwayRank (f . n) in ConwayRank (f . m) by A9; :: thesis: verum