let X1, X2 be Element of L; ( 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)) )
; 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)))
then reconsider P = P as Permutation of (dom (# (p1,x))) ;
A9:
# (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 A10:
t in # (
p2,
x)
;
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;
verum
end; let t be
object ;
( t in P * (# (p1,x)) implies t in # (p2,x) )assume A16:
t in P * (# (p1,x))
;
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;
verum end;
hence
# (
p2,
x)
= P * (# (p1,x))
;
verum
end;
the addF of L is commutative
by GROUP_1A:203;
hence
X1 = X2
by A9, A5, A7, FINSOP_1:7; verum