let X1, X2 be 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 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 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 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 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 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 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 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 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 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: rng P = dom q1 by A16, FUNCT_2:def 3;
A25: dom P = dom q2 by A19, A22, FUNCT_2:52;
A26: rng P = dom q2 by A19, A22, FUNCT_2:def 3;
A27: dom p1 = dom q2 by A10, A11, A13, A14, A19, Th1;
now :: thesis: for xd being object holds
( xd in dom (q1 * P) iff xd in dom q2 )
let xd be object ; :: 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:3;
hence ( xd in dom (q1 * P) iff xd in dom q2 ) by A25, FUNCT_1:11; :: thesis: verum
end;
then A28: dom q2 = dom (q1 * P) by TARSKI:2;
now :: thesis: for s being object st s in dom q2 holds
q2 . s = (q1 * P) . s
let s be object ; :: thesis: ( s in dom q2 implies q2 . s = (q1 * P) . s )
assume A29: 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, A26, A29, FUNCT_1:3;
then reconsider j = P . i as Element of NAT ;
A30: s in dom P by A19, A22, A29, FUNCT_2:52;
q2 . s = PO (i,p2,x) by A20, A29
.= PO (j,p1,x) by A23, A30, FUNCT_1:13
.= q1 . (P . i) by A16, A17, A25, A26, A27, A29, FUNCT_1:3
.= (q1 * P) . s by A30, FUNCT_1:13 ;
hence q2 . s = (q1 * P) . s ; :: thesis: verum
end;
then q2 = q1 * P by A28, FUNCT_1:2;
hence X1 = X2 by A16, A18, A21, FINSOP_1:7; :: thesis: verum