let g1, g2 be real-valued non-decreasing FinSequence; :: thesis: ( g1,g2 are_fiberwise_equipotent implies g1 = g2 )
len g1 = len g1 ;
hence ( g1,g2 are_fiberwise_equipotent implies g1 = g2 ) by Lm4; :: thesis: verum