let g1, g2 be real-valued non-increasing FinSequence; :: 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