let X1, X2 be Element of DX; :: thesis: ( ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & X1 = f "**" p ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & X2 = f "**" p ) implies X1 = X2 )
assume that
A5: ex p1 being FinSequence of DX st
( p1 is one-to-one & rng p1 = Y & X1 = f "**" p1 ) and
A6: ex p2 being FinSequence of DX st
( p2 is one-to-one & rng p2 = Y & X2 = f "**" p2 ) ; :: thesis: X1 = X2
consider p1 being FinSequence of DX such that
A7: p1 is one-to-one and
A8: rng p1 = Y and
A9: X1 = f "**" p1 by A5;
consider p2 being FinSequence of DX such that
A10: p2 is one-to-one and
A11: rng p2 = Y and
A12: X2 = f "**" p2 by A6;
ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) by A7, A8, A10, A11, Th1;
hence X1 = X2 by A1, A2, A9, A12, FINSOP_1:7; :: thesis: verum