let A, B be decreasing Ordinal-Sequence; :: thesis: for n being Nat st len A = n + 1 & rng A = rng B holds
A . n = B . n
let n be Nat; :: thesis: ( len A = n + 1 & rng A = rng B implies A . n = B . n )
assume A1: ( len A = n + 1 & rng A = rng B ) ; :: thesis: A . n = B . n
A2: dom A = card (dom A)
.= card (rng B) by A1, CARD_1:70
.= card (dom B) by CARD_1:70
.= dom B ;
n in succ n by ORDINAL1:6;
then A3: n in n + 1 by Lm5;
then A . n in rng B by A1, FUNCT_1:3;
then consider m being object such that
A4: ( m in dom B & B . m = A . n ) by FUNCT_1:def 3;
B . n in rng A by A1, A2, A3, FUNCT_1:3;
then consider k being object such that
A5: ( k in dom A & A . k = B . n ) by FUNCT_1:def 3;
reconsider m = m, k = k as Nat by A4, A5;
per cases ( m in k or m = k or k in m ) by ORDINAL1:14;
suppose m in k ; :: thesis: A . n = B . n
then A6: ( A . k in A . m & B . k in B . m ) by A2, A5, ORDINAL5:def 1;
k in succ n by A1, A5, Lm5;
per cases then ( k in n or k = n ) by ORDINAL1:8;
suppose k in n ; :: thesis: A . n = B . n
then ( A . n in A . k & B . n in B . k ) by A1, A2, A3, ORDINAL5:def 1;
hence A . n = B . n by A4, A5, A6, ORDINAL1:10; :: thesis: verum
end;
suppose k = n ; :: thesis: A . n = B . n
hence A . n = B . n by A5; :: thesis: verum
end;
end;
end;
suppose A7: m = k ; :: thesis: A . n = B . n
k in succ n by A1, A5, Lm5;
per cases then ( k in n or k = n ) by ORDINAL1:8;
suppose k in n ; :: thesis: A . n = B . n
then ( A . n in A . k & B . n in B . k ) by A1, A2, A3, ORDINAL5:def 1;
hence A . n = B . n by A4, A5, A7; :: thesis: verum
end;
suppose k = n ; :: thesis: A . n = B . n
hence A . n = B . n by A4, A7; :: thesis: verum
end;
end;
end;
suppose k in m ; :: thesis: A . n = B . n
then A8: ( A . m in A . k & B . m in B . k ) by A2, A4, ORDINAL5:def 1;
m in succ n by A1, A2, A4, Lm5;
per cases then ( m in n or m = n ) by ORDINAL1:8;
suppose m in n ; :: thesis: A . n = B . n
then ( A . n in A . m & B . n in B . m ) by A1, A2, A3, ORDINAL5:def 1;
hence A . n = B . n by A4, A5, A8, ORDINAL1:10; :: thesis: verum
end;
suppose m = n ; :: thesis: A . n = B . n
hence A . n = B . n by A4; :: thesis: verum
end;
end;
end;
end;