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
A3: ex p1 being FinSequence of DX st
( p1 is one-to-one & rng p1 = Y & X1 = f "**" p1 ) and
A4: 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
A5: p1 is one-to-one and
A6: rng p1 = Y and
A7: X1 = f "**" p1 by A3;
consider p2 being FinSequence of DX such that
A8: p2 is one-to-one and
A9: rng p2 = Y and
A10: X2 = f "**" p2 by A4;
ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) by A5, A6, A8, A9, Th1;
hence X1 = X2 by A1, A2, A7, A10, FINSOP_1:7; :: thesis: verum