defpred S3[ Nat] means for g1, g2 being non-increasing FinSequence of REAL st $1 = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2;
A1:
for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be
Nat;
( S3[n] implies S3[n + 1] )
assume A2:
S3[
n]
;
S3[n + 1]
let g1,
g2 be
non-increasing FinSequence of
REAL ;
( n + 1 = len g1 & g1,g2 are_fiberwise_equipotent implies g1 = g2 )
set r =
g1 . (n + 1);
reconsider g1n =
g1 | n,
g2n =
g2 | n as
non-increasing FinSequence of
REAL by Th20;
assume that A3:
len g1 = n + 1
and A4:
g1,
g2 are_fiberwise_equipotent
;
g1 = g2
A5:
len g2 = len g1
by A4, Th3;
then A6:
g1 . (len g1) = g2 . (len g2)
by A3, A4, Lm4;
A7:
(g1 | n) ^ <*(g1 . (n + 1))*> = g1
by A3, Th7;
len (g1 | n) = n
by A3, FINSEQ_1:59, NAT_1:11;
then
g1n = g2n
by A2, A3, A4, A5, Lm4;
hence
g1 = g2
by A3, A5, A6, A7, Th7;
verum
end;
A8:
S3[ 0 ]
thus
for n being Nat holds S3[n]
from NAT_1:sch 2(A8, A1); verum