let X be 1 -element FinSequence; :: thesis: ( not X . 1 is empty implies ex I being Function of (X . 1),(product X) st
( I is one-to-one & I is onto & ( for x being object st x in X . 1 holds
I . x = <*x*> ) ) )
assume not X . 1 is empty ; :: thesis: ex I being Function of (X . 1),(product X) st
( I is one-to-one & I is onto & ( for x being object st x in X . 1 holds
I . x = <*x*> ) )
then ( dom X = {1} & X . 1 is non empty set ) by FINSEQ_1:2, FINSEQ_1:89;
hence ex I being Function of (X . 1),(product X) st
( I is one-to-one & I is onto & ( for x being object st x in X . 1 holds
I . x = <*x*> ) ) by PRVECT_3:2; :: thesis: verum