defpred S_{3}[ 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 S_{3}[n] holds

S_{3}[n + 1]
_{3}[ 0 ]
_{3}[n]
from NAT_1:sch 2(A8, A1); :: thesis: verum

g1 = g2;

A1: for n being Nat st S

S

proof

A8:
S
let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[n + 1] )

assume A2: S_{3}[n]
; :: thesis: S_{3}[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;assume A2: S

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

proof

thus
for n being Nat holds S
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;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