let X1, X2 be Element of L; :: thesis: ( ex p being one-to-one FinSequence of I st
( rng p = J & X1 = the multF of L "**" (# (p,x)) ) & ex p being one-to-one FinSequence of I st
( rng p = J & X2 = the multF 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 multF of L "**" (# (p1,x)) ) and
A3: ex p2 being one-to-one FinSequence of I st
( rng p2 = J & X2 = the multF 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 multF 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 multF 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))) ;
# (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 A9: t in # (p2,x) ; :: thesis: t in P * (# (p1,x))
consider a, b being object such that
A10: t = [a,b] by A9, RELAT_1:def 1;
consider z being object such that
A11: [a,z] in p2 and
A12: [z,b] in x by A9, A10, RELAT_1:def 8;
consider y being object such that
A13: [a,y] in P and
A14: [y,z] in p1 by A11, A8, RELAT_1:def 8;
( [a,y] in P & [y,b] in p1 * x ) by A13, A12, A14, RELAT_1:def 8;
hence t in P * (# (p1,x)) by A10, RELAT_1:def 8; :: thesis: verum

end;

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

end;

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

end;

hence X1 = X2 by A5, A7, FINSOP_1:7; :: thesis: verum