let f, g be FinSequence; :: thesis: ( rng f = rng g implies ( len f = 0 iff len g = 0 ) )
assume A1: rng f = rng g ; :: thesis: ( len f = 0 iff len g = 0 )

hereby :: thesis: ( len g = 0 implies len f = 0 )

assume len f = 0 ; :: thesis: len g = 0
then f = {} ;
then g = {} by RELAT_1:38, A1, RELAT_1:41;
hence len g = 0 ; :: thesis: verum

end;

assume len g = 0 ; :: thesis: len f = 0
then g = {} ;
then f = {} by RELAT_1:38, A1, RELAT_1:41;
hence len f = 0 ; :: thesis: verum