let X1, X2 be Element of X; :: thesis: ( ex p being FinSequence of the carrier of X st

( p is one-to-one & rng p = Y & X1 = the addF of X "**" p ) & ex p being FinSequence of the carrier of X st

( p is one-to-one & rng p = Y & X2 = the addF of X "**" p ) implies X1 = X2 )

assume that

A4: ex p1 being FinSequence of the carrier of X st

( p1 is one-to-one & rng p1 = Y & X1 = the addF of X "**" p1 ) and

A5: ex p2 being FinSequence of the carrier of X st

( p2 is one-to-one & rng p2 = Y & X2 = the addF of X "**" p2 ) ; :: thesis: X1 = X2

consider p2 being FinSequence of the carrier of X such that

A6: ( p2 is one-to-one & rng p2 = Y ) and

A7: X2 = the addF of X "**" p2 by A5;

consider p1 being FinSequence of the carrier of X such that

A8: ( p1 is one-to-one & rng p1 = Y ) and

A9: X1 = the addF of X "**" p1 by A4;

ex P being Permutation of (dom p1) st

( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) by A8, A6, BHSP_5:1;

hence X1 = X2 by A1, A9, A7, FINSOP_1:7; :: thesis: verum

( p is one-to-one & rng p = Y & X1 = the addF of X "**" p ) & ex p being FinSequence of the carrier of X st

( p is one-to-one & rng p = Y & X2 = the addF of X "**" p ) implies X1 = X2 )

assume that

A4: ex p1 being FinSequence of the carrier of X st

( p1 is one-to-one & rng p1 = Y & X1 = the addF of X "**" p1 ) and

A5: ex p2 being FinSequence of the carrier of X st

( p2 is one-to-one & rng p2 = Y & X2 = the addF of X "**" p2 ) ; :: thesis: X1 = X2

consider p2 being FinSequence of the carrier of X such that

A6: ( p2 is one-to-one & rng p2 = Y ) and

A7: X2 = the addF of X "**" p2 by A5;

consider p1 being FinSequence of the carrier of X such that

A8: ( p1 is one-to-one & rng p1 = Y ) and

A9: X1 = the addF of X "**" p1 by A4;

ex P being Permutation of (dom p1) st

( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) by A8, A6, BHSP_5:1;

hence X1 = X2 by A1, A9, A7, FINSOP_1:7; :: thesis: verum