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; :: thesis: ( S3[n] implies S3[n + 1] )
assume A2: S3[n] ; :: thesis: S3[n + 1]
let g1, g2 be non-increasing FinSequence of REAL ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
A8: S3[ 0 ]
proof
let g1, g2 be non-increasing FinSequence of REAL ; :: thesis: ( 0 = len g1 & g1,g2 are_fiberwise_equipotent implies g1 = g2 )
assume ( len g1 = 0 & g1,g2 are_fiberwise_equipotent ) ; :: thesis: g1 = g2
then ( len g2 = len g1 & g1 = <*> REAL ) by Th3;
hence g1 = g2 ; :: thesis: verum
end;
thus for n being Nat holds S3[n] from NAT_1:sch 2(A8, A1); :: thesis: verum