let X1, X2 be Element of DK; ( 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
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) )
; X1 = X2
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;
then A16:
dom (Func_Seq F,p1) = dom p1
by TARSKI:2;
then A17:
dom (Func_Seq F,p2) = dom p2
by TARSKI:2;
A18:
rng P = dom (Func_Seq F,p1)
by A16, FUNCT_2:def 3;
then A19:
dom (Func_Seq F,p2) = dom ((Func_Seq F,p1) * P)
by TARSKI:2;
now let s be
set ;
( s in dom (Func_Seq F,p2) implies (Func_Seq F,p2) . s = ((Func_Seq F,p1) * P) . s )assume A20:
s in dom (Func_Seq F,p2)
;
(Func_Seq F,p2) . s = ((Func_Seq F,p1) * P) . sthen reconsider i =
s as
Element of
NAT ;
i in dom P
by A14, A17, A20, FUNCT_2:67;
then A21:
P . i in rng P
by FUNCT_1:12;
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:67;
(Func_Seq F,p2) . s =
F . (p2 . i)
by A17, A20, FUNCT_1:23
.=
F . (p1 . (P . i))
by A15, A23, FUNCT_1:23
.=
(Func_Seq F,p1) . j
by A22, FUNCT_1:23
.=
((Func_Seq F,p1) * P) . s
by A23, FUNCT_1:23
;
hence
(Func_Seq F,p2) . s = ((Func_Seq F,p1) * P) . s
;
verum end;
then
Func_Seq F,p2 = (Func_Seq F,p1) * P
by A19, FUNCT_1:9;
hence
X1 = X2
by A1, A2, A10, A13, A16, FINSOP_1:8; verum