let X be non empty set ; for P being a_partition of X
for p being FinSequence of P
for q1, q2 being FinSequence
for x, y being set st (q1 ^ <*x*>) ^ q2 in product p & ex a being Element of P st
( x in a & y in a ) holds
(q1 ^ <*y*>) ^ q2 in product p
let P be a_partition of X; for p being FinSequence of P
for q1, q2 being FinSequence
for x, y being set st (q1 ^ <*x*>) ^ q2 in product p & ex a being Element of P st
( x in a & y in a ) holds
(q1 ^ <*y*>) ^ q2 in product p
let pp be FinSequence of P; for q1, q2 being FinSequence
for x, y being set st (q1 ^ <*x*>) ^ q2 in product pp & ex a being Element of P st
( x in a & y in a ) holds
(q1 ^ <*y*>) ^ q2 in product pp
let p, q be FinSequence; for x, y being set st (p ^ <*x*>) ^ q in product pp & ex a being Element of P st
( x in a & y in a ) holds
(p ^ <*y*>) ^ q in product pp
let x, y be set ; ( (p ^ <*x*>) ^ q in product pp & ex a being Element of P st
( x in a & y in a ) implies (p ^ <*y*>) ^ q in product pp )
assume A1:
(p ^ <*x*>) ^ q in product pp
; ( for a being Element of P holds
( not x in a or not y in a ) or (p ^ <*y*>) ^ q in product pp )
given a being Element of P such that A2:
x in a
and
A3:
y in a
; (p ^ <*y*>) ^ q in product pp
reconsider x = x, y = y as Element of a by A2, A3;
now ( dom ((p ^ <*y*>) ^ q) = dom pp & ( for i being object st i in dom pp holds
((p ^ <*y*>) ^ q) . i in pp . i ) )A4:
ex
g being
Function st
(
(p ^ <*x*>) ^ q = g &
dom g = dom pp & ( for
x being
object st
x in dom pp holds
g . x in pp . x ) )
by A1, CARD_3:def 5;
thus dom ((p ^ <*y*>) ^ q) =
Seg (len ((p ^ <*y*>) ^ q))
by FINSEQ_1:def 3
.=
Seg ((len (p ^ <*y*>)) + (len q))
by FINSEQ_1:22
.=
Seg (((len p) + (len <*y*>)) + (len q))
by FINSEQ_1:22
.=
Seg (((len p) + 1) + (len q))
by FINSEQ_1:40
.=
Seg (((len p) + (len <*x*>)) + (len q))
by FINSEQ_1:40
.=
Seg ((len (p ^ <*x*>)) + (len q))
by FINSEQ_1:22
.=
Seg (len ((p ^ <*x*>) ^ q))
by FINSEQ_1:22
.=
dom pp
by A4, FINSEQ_1:def 3
;
for i being object st i in dom pp holds
((p ^ <*y*>) ^ q) . b2 in pp . b2let i be
object ;
( i in dom pp implies ((p ^ <*y*>) ^ q) . b1 in pp . b1 )assume A5:
i in dom pp
;
((p ^ <*y*>) ^ q) . b1 in pp . b1then reconsider ii =
i as
Element of
NAT ;
A6:
len <*x*> = 1
by FINSEQ_1:40;
A7:
len <*y*> = 1
by FINSEQ_1:40;
A8:
dom <*x*> = Seg 1
by FINSEQ_1:38;
A9:
len (p ^ <*x*>) = (len p) + 1
by A6, FINSEQ_1:22;
A10:
len (p ^ <*y*>) = (len p) + 1
by A7, FINSEQ_1:22;
A11:
dom (p ^ <*x*>) = Seg ((len p) + 1)
by A9, FINSEQ_1:def 3;
A12:
dom (p ^ <*y*>) = Seg ((len p) + 1)
by A10, FINSEQ_1:def 3;
A13:
(
ii in dom (p ^ <*x*>) or ex
n being
Nat st
(
n in dom q &
ii = (len (p ^ <*x*>)) + n ) )
by A4, A5, FINSEQ_1:25;
A14:
dom p c= dom (p ^ <*y*>)
by FINSEQ_1:26;
per cases
( ii in dom p or ex n being Nat st
( n in dom <*x*> & ii = (len p) + n ) or ex n being Element of NAT st
( n in dom q & ii = (len (p ^ <*x*>)) + n ) )
by A13, FINSEQ_1:25;
suppose A15:
ii in dom p
;
((p ^ <*y*>) ^ q) . b1 in pp . b1then A16:
(p ^ <*y*>) . i = p . i
by FINSEQ_1:def 7;
A17:
(p ^ <*x*>) . i = p . i
by A15, FINSEQ_1:def 7;
A18:
((p ^ <*y*>) ^ q) . i = p . i
by A14, A15, A16, FINSEQ_1:def 7;
((p ^ <*x*>) ^ q) . i = p . i
by A11, A12, A14, A15, A17, FINSEQ_1:def 7;
hence
((p ^ <*y*>) ^ q) . i in pp . i
by A4, A5, A18;
verum end; suppose
ex
n being
Nat st
(
n in dom <*x*> &
ii = (len p) + n )
;
((p ^ <*y*>) ^ q) . b1 in pp . b1then consider n being
Nat such that A19:
n in Seg 1
and A20:
ii = (len p) + n
by A8;
A21:
n = 1
by A19, FINSEQ_1:2, TARSKI:def 1;
then A22:
(p ^ <*x*>) . ii = x
by A20, FINSEQ_1:42;
A23:
(p ^ <*y*>) . ii = y
by A20, A21, FINSEQ_1:42;
A24:
ii in dom (p ^ <*y*>)
by A12, A20, A21, FINSEQ_1:4;
then A25:
((p ^ <*x*>) ^ q) . ii = x
by A11, A12, A22, FINSEQ_1:def 7;
A26:
((p ^ <*y*>) ^ q) . ii = y
by A23, A24, FINSEQ_1:def 7;
A27:
x in pp . i
by A4, A5, A25;
pp . i in rng pp
by A5, FUNCT_1:def 3;
then A28:
pp . i in P
;
a meets pp . i
by A27, XBOOLE_0:3;
then
pp . i = a
by A28, EQREL_1:def 4;
hence
((p ^ <*y*>) ^ q) . i in pp . i
by A26;
verum end; end;
hence
(p ^ <*y*>) ^ q in product pp
by CARD_3:def 5; verum