let X1, X2 be Element of REAL ; :: thesis: ( ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO i,p,x ) & X1 = addreal "**" q ) ) & ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Element of NAT st i in dom q holds
q . i = PO i,p,x ) & X2 = addreal "**" q ) ) implies X1 = X2 )
assume that
A8: ex p1 being FinSequence of the carrier of X st
( p1 is one-to-one & rng p1 = Y & ex q1 being FinSequence of REAL st
( dom q1 = dom p1 & ( for i being Element of NAT st i in dom q1 holds
q1 . i = PO i,p1,x ) & X1 = addreal "**" q1 ) ) and
A9: ex p2 being FinSequence of the carrier of X st
( p2 is one-to-one & rng p2 = Y & ex q2 being FinSequence of REAL st
( dom q2 = dom p2 & ( for i being Element of NAT st i in dom q2 holds
q2 . i = PO i,p2,x ) & X2 = addreal "**" q2 ) ) ; :: thesis: X1 = X2
consider p1 being FinSequence of the carrier of X such that
A10: p1 is one-to-one and
A11: rng p1 = Y and
A12: ex q1 being FinSequence of REAL st
( dom q1 = dom p1 & ( for i being Element of NAT st i in dom q1 holds
q1 . i = PO i,p1,x ) & X1 = addreal "**" q1 ) by A8;
consider p2 being FinSequence of the carrier of X such that
A13: p2 is one-to-one and
A14: rng p2 = Y and
A15: ex q2 being FinSequence of REAL st
( dom q2 = dom p2 & ( for i being Element of NAT st i in dom q2 holds
q2 . i = PO i,p2,x ) & X2 = addreal "**" q2 ) by A9;
consider q1 being FinSequence of REAL such that
A16: dom q1 = dom p1 and
A17: for i being Element of NAT st i in dom q1 holds
q1 . i = PO i,p1,x and
A18: X1 = addreal "**" q1 by A12;
consider q2 being FinSequence of REAL such that
A19: dom q2 = dom p2 and
A20: for i being Element of NAT st i in dom q2 holds
q2 . i = PO i,p2,x and
A21: X2 = addreal "**" q2 by A15;
A22: ( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) ) by A10, A11, A13, A14, Th1;
consider P being Permutation of (dom p1) such that
A23: p2 = p1 * P and
dom P = dom p1 and
rng P = dom p1 by A10, A11, A13, A14, Th1;
A24: ( dom P = dom q1 & rng P = dom q1 ) by A16, FUNCT_2:67, FUNCT_2:def 3;
A25: ( dom P = dom q2 & rng P = dom q2 ) by A19, A22, FUNCT_2:67, FUNCT_2:def 3;
A26: dom p1 = dom q2 by A10, A11, A13, A14, A19, Th1;

now

let xd be set ; :: thesis: ( xd in dom (q1 * P) iff xd in dom q2 )
( xd in dom P implies P . xd in dom q1 ) by A24, FUNCT_1:12;
hence ( xd in dom (q1 * P) iff xd in dom q2 ) by A25, FUNCT_1:21; :: thesis: verum

end;

then A27: dom q2 = dom (q1 * P) by TARSKI:2;
q2 = q1 * P

proof

now

let s be set ; :: thesis: ( s in dom q2 implies q2 . s = (q1 * P) . s )
assume A28: s in dom q2 ; :: thesis: q2 . s = (q1 * P) . s
then reconsider i = s as Element of NAT ;
P . i in dom q2 by A25, A28, FUNCT_1:12;
then reconsider j = P . i as Element of NAT ;
A29: s in dom P by A19, A22, A28, FUNCT_2:67;
q2 . s = PO i,p2,x by A20, A28
.= PO j,p1,x by A23, A29, FUNCT_1:23
.= q1 . (P . i) by A16, A17, A25, A26, A28, FUNCT_1:12
.= (q1 * P) . s by A29, FUNCT_1:23 ;
hence q2 . s = (q1 * P) . s ; :: thesis: verum

end;

hence q2 = q1 * P by A27, FUNCT_1:9; :: thesis: verum

end;

hence X1 = X2 by A16, A18, A21, FINSOP_1:8; :: thesis: verum