let X1, X2 be Element of L; :: thesis: ( ex p being one-to-one FinSequence of I st
( rng p = J & X1 = the addF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st
( rng p = J & X2 = the addF of L "**" (# (p,x)) ) implies X1 = X2 )
assume that
A2: ex p1 being one-to-one FinSequence of I st
( rng p1 = J & X1 = the addF of L "**" (# (p1,x)) ) and
A3: ex p2 being one-to-one FinSequence of I st
( rng p2 = J & X2 = the addF of L "**" (# (p2,x)) ) ; :: thesis: X1 = X2
consider p1 being one-to-one FinSequence of I such that
A4: rng p1 = J and
A5: X1 = the addF of L "**" (# (p1,x)) by A2;
consider p2 being one-to-one FinSequence of I such that
A6: rng p2 = J and
A7: X2 = the addF of L "**" (# (p2,x)) by A3;
consider P being Permutation of (dom p1) such that
A8: ( p2 = P * p1 & dom P = dom p1 & rng P = dom p1 ) by A4, A6, BHSP_5:1;
P is Permutation of (dom (# (p1,x)))

proof

dom x = I by PARTFUN1:def 2;
then rng p1 c= dom x by FINSEQ_1:def 4;
then dom (p1 * x) = dom p1 by RELAT_1:27;
hence P is Permutation of (dom (# (p1,x))) ; :: thesis: verum

end;

then reconsider P = P as Permutation of (dom (# (p1,x))) ;
A9: # (p2,x) = P * (# (p1,x))

proof

now :: thesis: ( ( for t being object st t in # (p2,x) holds
t in P * (# (p1,x)) ) & ( for t being object st t in P * (# (p1,x)) holds
t in # (p2,x) ) )

hereby :: thesis: for t being object st t in P * (# (p1,x)) holds
t in # (p2,x)

let t be object ; :: thesis: ( t in # (p2,x) implies t in P * (# (p1,x)) )
assume A10: t in # (p2,x) ; :: thesis: t in P * (# (p1,x))
consider a, b being object such that
A11: t = [a,b] by A10, RELAT_1:def 1;
consider z being object such that
A12: [a,z] in p2 and
A13: [z,b] in x by A10, A11, RELAT_1:def 8;
consider y being object such that
A14: [a,y] in P and
A15: [y,z] in p1 by A12, A8, RELAT_1:def 8;
( [a,y] in P & [y,b] in p1 * x ) by A14, A13, A15, RELAT_1:def 8;
hence t in P * (# (p1,x)) by A11, RELAT_1:def 8; :: thesis: verum

end;

let t be object ; :: thesis: ( t in P * (# (p1,x)) implies t in # (p2,x) )
assume A16: t in P * (# (p1,x)) ; :: thesis: t in # (p2,x)
then consider a, b being object such that
A17: t = [a,b] by RELAT_1:def 1;
consider c being object such that
A18: [a,c] in P and
A19: [c,b] in p1 * x by A16, A17, RELAT_1:def 8;
consider d being object such that
A20: [c,d] in p1 and
A21: [d,b] in x by A19, RELAT_1:def 8;
[a,d] in p2 by A8, RELAT_1:def 8, A18, A20;
hence t in # (p2,x) by A17, A21, RELAT_1:def 8; :: thesis: verum

end;

hence # (p2,x) = P * (# (p1,x)) ; :: thesis: verum

end;

the addF of L is commutative by GROUP_1A:203;
hence X1 = X2 by A9, A5, A7, FINSOP_1:7; :: thesis: verum