let X1, X2 be Element of L; :: thesis:
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:
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)))

end;

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

let t be object ; :: thesis:
assume A10: t in # (p2,x) ; :: thesis:
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:

end;

let t be object ; :: thesis:
assume A16: t in P * (# (p1,x)) ; :: thesis:
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:

end;

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

end;