let X1, X2 be Element of L; ( 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)) )
; 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)))
then reconsider P = P as Permutation of (dom (# (p1,x))) ;
# (p2,x) = P * (# (p1,x))
proof
now ( ( 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 for t being object st t in P * (# (p1,x)) holds
t in # (p2,x)
let t be
object ;
( t in # (p2,x) implies t in P * (# (p1,x)) )assume A9:
t in # (
p2,
x)
;
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;
verum
end; let t be
object ;
( t in P * (# (p1,x)) implies t in # (p2,x) )assume A15:
t in P * (# (p1,x))
;
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;
verum end;
hence
# (
p2,
x)
= P * (# (p1,x))
;
verum
end;
hence
X1 = X2
by A5, A7, FINSOP_1:7; verum