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)))

# (p2,x) = P * (# (p1,x))

( 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

then reconsider P = P as Permutation of (dom (# (p1,x))) ;
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 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

# (p2,x) = P * (# (p1,x))

proof

end;

hence
X1 = X2
by A5, A7, FVSUM_1:8, FINSOP_1:7; :: thesis: verumnow :: 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) ) )

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: verumt 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 P * (# (p1,x)) implies t in # (p2,x) )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;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

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