let g1, g2 be non-increasing FinSequence of REAL ; :: thesis: ( g1,g2 are_fiberwise_equipotent implies g1 = g2 )
A1: len g1 = len g1 ;
assume g1,g2 are_fiberwise_equipotent ; :: thesis: g1 = g2
hence g1 = g2 by A1, Lm7; :: thesis: verum