let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( (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 ; :: thesis: ( 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 & y in a ) ; :: thesis: (p ^ <*y*>) ^ q in product pp
reconsider x = x, y = y as Element of a by A2;

now

A3: ex g being Function st
( (p ^ <*x*>) ^ q = g & dom g = dom pp & ( for x being set 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:35
.= Seg (((len p) + (len <*y*>)) + (len q)) by FINSEQ_1:35
.= Seg (((len p) + 1) + (len q)) by FINSEQ_1:57
.= Seg (((len p) + (len <*x*>)) + (len q)) by FINSEQ_1:57
.= Seg ((len (p ^ <*x*>)) + (len q)) by FINSEQ_1:35
.= Seg (len ((p ^ <*x*>) ^ q)) by FINSEQ_1:35
.= dom pp by A3, FINSEQ_1:def 3 ; :: thesis: for i being set st i in dom pp holds
((p ^ <*y*>) ^ q) . b₂ in pp . b₂
let i be set ; :: thesis: ( i in dom pp implies ((p ^ <*y*>) ^ q) . b₁ in pp . b₁ )
assume A4: i in dom pp ; :: thesis: ((p ^ <*y*>) ^ q) . b₁ in pp . b₁
then reconsider ii = i as Element of NAT ;
A5: ( len <*x*> = 1 & len <*y*> = 1 & dom <*x*> = Seg 1 & dom <*y*> = Seg 1 ) by FINSEQ_1:55, FINSEQ_1:57;
then A6: ( len (p ^ <*x*>) = (len p) + 1 & len (p ^ <*y*>) = (len p) + 1 ) by FINSEQ_1:35;
then A7: ( dom (p ^ <*x*>) = Seg ((len p) + 1) & dom (p ^ <*y*>) = Seg ((len p) + 1) ) by FINSEQ_1:def 3;
A8: ( ii in dom (p ^ <*x*>) or ex n being Nat st
( n in dom q & ii = (len (p ^ <*x*>)) + n ) ) by A3, A4, FINSEQ_1:38;
A9: ( dom p c= dom (p ^ <*y*>) & dom (p ^ <*y*>) c= dom ((p ^ <*y*>) ^ q) ) by FINSEQ_1:39;

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 A8, FINSEQ_1:38;

suppose ii in dom p ; :: thesis: ((p ^ <*y*>) ^ q) . b₁ in pp . b₁

then ( (p ^ <*y*>) . i = p . i & (p ^ <*x*>) . i = p . i & ii in dom (p ^ <*y*>) ) by A9, FINSEQ_1:def 7;
then ( ((p ^ <*y*>) ^ q) . i = p . i & ((p ^ <*x*>) ^ q) . i = p . i ) by A7, FINSEQ_1:def 7;
hence ((p ^ <*y*>) ^ q) . i in pp . i by A3, A4; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom <*x*> & ii = (len p) + n ) ; :: thesis: ((p ^ <*y*>) ^ q) . b₁ in pp . b₁

then consider n being Nat such that
A10: ( n in Seg 1 & ii = (len p) + n ) by A5;
n = 1 by A10, FINSEQ_1:4, TARSKI:def 1;
then ( (p ^ <*x*>) . ii = x & (p ^ <*y*>) . ii = y & ii in dom (p ^ <*y*>) ) by A7, A10, FINSEQ_1:6, FINSEQ_1:59;
then A11: ( ((p ^ <*x*>) ^ q) . ii = x & ((p ^ <*y*>) ^ q) . ii = y ) by A7, FINSEQ_1:def 7;
then ( x in pp . i & pp . i in rng pp & rng pp c= P ) by A3, A4, FUNCT_1:def 5;
then ( pp . i in P & a meets pp . i ) by XBOOLE_0:3;
then pp . i = a by EQREL_1:def 6;
hence ((p ^ <*y*>) ^ q) . i in pp . i by A11; :: thesis: verum

end;

suppose ex n being Element of NAT st
( n in dom q & ii = (len (p ^ <*x*>)) + n ) ; :: thesis: ((p ^ <*y*>) ^ q) . b₁ in pp . b₁

then consider n being Element of NAT such that
A12: ( n in dom q & ii = (len (p ^ <*x*>)) + n ) ;
( ((p ^ <*y*>) ^ q) . i = q . n & ((p ^ <*x*>) ^ q) . i = q . n ) by A6, A12, FINSEQ_1:def 7;
hence ((p ^ <*y*>) ^ q) . i in pp . i by A3, A4; :: thesis: verum

end;

end;

end;

hence (p ^ <*y*>) ^ q in product pp by CARD_3:def 5; :: thesis: verum