defpred S₃[ Nat] means for g1, g2 being real-valued non-increasing FinSequence st $1 = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2;
A1: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

let n be Nat; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume A2: S₃[n] ; :: thesis: S₃[n + 1]
let g1, g2 be real-valued non-increasing FinSequence; :: 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 real-valued non-increasing FinSequence ;
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: S₃[ 0 ]

proof

let g1, g2 be real-valued non-increasing FinSequence; :: 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 S₃[n] from NAT_1:sch 2(A8, A1); :: thesis: verum