let X1, X2 be Element of DK; :: thesis:
assume that
A6: ex p1 being FinSequence of DX st
( p1 is one-to-one & rng p1 = Y & X1 = f "**" (Func_Seq (F,p1)) ) and
A7: ex p2 being FinSequence of DX st
( p2 is one-to-one & rng p2 = Y & X2 = f "**" (Func_Seq (F,p2)) ) ; :: thesis:
consider p1 being FinSequence of DX such that
A8: p1 is one-to-one and
A9: rng p1 = Y and
A10: X1 = f "**" (Func_Seq (F,p1)) by A6;
consider p2 being FinSequence of DX such that
A11: p2 is one-to-one and
A12: rng p2 = Y and
A13: X2 = f "**" (Func_Seq (F,p2)) by A7;
A14: dom p1 = dom p2 by A8, A9, A11, A12, Th1;
consider P being Permutation of (dom p1) such that
A15: p2 = p1 * P and
dom P = dom p1 and
rng P = dom p1 by A8, A9, A11, A12, Th1;

let xd be object ; :: thesis:
( 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 A3, A9, FUNCT_1:11; :: thesis:

end;

let xd be object ; :: thesis:
( 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 A3, A12, FUNCT_1:11; :: thesis:

end;

end;

let s be object ; :: thesis:
assume A20: s in dom (Func_Seq (F,p2)) ; :: thesis:
then reconsider i = s as Element of NAT ;
i in dom P by A14, A17, A20, FUNCT_2:52;
then A21: P . i in rng P by FUNCT_1:3;
then P . i in dom (Func_Seq (F,p2)) by A14, A17, FUNCT_2:def 3;
then reconsider j = P . i as Element of NAT ;
A22: j in dom p1 by A21, FUNCT_2:def 3;
A23: s in dom P by A14, A17, A20, FUNCT_2:52;
(Func_Seq (F,p2)) . s = F . (p2 . i) by A17, A20, FUNCT_1:13
.= F . (p1 . (P . i)) by A15, A23, FUNCT_1:13
.= (Func_Seq (F,p1)) . j by A22, FUNCT_1:13
.= ((Func_Seq (F,p1)) * P) . s by A23, FUNCT_1:13 ;
hence (Func_Seq (F,p2)) . s = ((Func_Seq (F,p1)) * P) . s ; :: thesis:

end;