let X1, X2 be Element of X; ( 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 )
; 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; verum