let X1, X2 be Element of DK; :: thesis: ( ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & X1 = f "**" (Func_Seq (F,p)) ) & ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & X2 = f "**" (Func_Seq (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 "**" (Func_Seq (F,p1)) ) and
A4: ex p2 being FinSequence of DX st
( p2 is one-to-one & rng p2 = Y & X2 = f "**" (Func_Seq (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 "**" (Func_Seq (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 "**" (Func_Seq (F,p2)) by A4;
A11: dom p1 = dom p2 by A5, A6, A8, A9, Th1;
consider P being Permutation of (dom p1) such that
A12: p2 = p1 * P and
dom P = dom p1 and
rng P = dom p1 by A5, A6, A8, A9, Th1;

now :: thesis: for xd being set holds
( xd in dom (Func_Seq (F,p1)) iff xd in dom p1 )

let xd be set ; :: thesis: ( xd in dom (Func_Seq (F,p1)) iff xd in dom p1 )
( xd in dom p1 implies p1 . xd in rng p1 ) by FUNCT_1:3;
hence ( xd in dom (Func_Seq (F,p1)) iff xd in dom p1 ) by B3, A6, FUNCT_1:11; :: thesis: verum

end;

then A13: dom (Func_Seq (F,p1)) = dom p1 by TARSKI:1;

now :: thesis: for xd being set holds
( xd in dom (Func_Seq (F,p2)) iff xd in dom p2 )

let xd be set ; :: thesis: ( xd in dom (Func_Seq (F,p2)) iff xd in dom p2 )
( xd in dom p2 implies p2 . xd in rng p2 ) by FUNCT_1:3;
hence ( xd in dom (Func_Seq (F,p2)) iff xd in dom p2 ) by B3, A9, FUNCT_1:11; :: thesis: verum

end;

then A14: dom (Func_Seq (F,p2)) = dom p2 by TARSKI:1;
A15: rng P = dom (Func_Seq (F,p1)) by A13, FUNCT_2:def 3;

now :: thesis: for xd being set holds
( xd in dom ((Func_Seq (F,p1)) * P) iff xd in dom (Func_Seq (F,p2)) )

let xd be set ; :: thesis: ( xd in dom ((Func_Seq (F,p1)) * P) iff xd in dom (Func_Seq (F,p2)) )
( xd in dom P implies P . xd in dom (Func_Seq (F,p1)) ) by A15, FUNCT_1:3;
then ( xd in dom ((Func_Seq (F,p1)) * P) iff xd in dom P ) by FUNCT_1:11;
hence ( xd in dom ((Func_Seq (F,p1)) * P) iff xd in dom (Func_Seq (F,p2)) ) by A11, A14, FUNCT_2:52; :: thesis: verum

end;

then A16: dom (Func_Seq (F,p2)) = dom ((Func_Seq (F,p1)) * P) by TARSKI:1;

now :: thesis: for s being set st s in dom (Func_Seq (F,p2)) holds
(Func_Seq (F,p2)) . s = ((Func_Seq (F,p1)) * P) . s

let s be set ; :: thesis: ( s in dom (Func_Seq (F,p2)) implies (Func_Seq (F,p2)) . s = ((Func_Seq (F,p1)) * P) . s )
assume A17: s in dom (Func_Seq (F,p2)) ; :: thesis: (Func_Seq (F,p2)) . s = ((Func_Seq (F,p1)) * P) . s
then reconsider i = s as Element of NAT ;
i in dom P by A11, A14, A17, FUNCT_2:52;
then A18: P . i in rng P by FUNCT_1:3;
then P . i in dom (Func_Seq (F,p2)) by A11, A14, FUNCT_2:def 3;
then reconsider j = P . i as Element of NAT ;
A19: j in dom p1 by A18, FUNCT_2:def 3;
A20: s in dom P by A11, A14, A17, FUNCT_2:52;
(Func_Seq (F,p2)) . s = F . (p2 . i) by A14, A17, FUNCT_1:13
.= F . (p1 . (P . i)) by A12, A20, FUNCT_1:13
.= (Func_Seq (F,p1)) . j by A19, FUNCT_1:13
.= ((Func_Seq (F,p1)) * P) . s by A20, FUNCT_1:13 ;
hence (Func_Seq (F,p2)) . s = ((Func_Seq (F,p1)) * P) . s ; :: thesis: verum

end;

then Func_Seq (F,p2) = (Func_Seq (F,p1)) * P by A16, FUNCT_1:2;
hence X1 = X2 by A1, A2, A7, A10, A13, FINSOP_1:7; :: thesis: verum