let X, Y be non empty set ; :: thesis: for F being disjoint_valued FinSequence of bool [:X,Y:]
for p being set holds
( ex Fy being disjoint_valued FinSequence of bool X st
( dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Y-section ((F . n),p) ) ) & ex Fx being disjoint_valued FinSequence of bool Y st
( dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = X-section ((F . n),p) ) ) )
let F be disjoint_valued FinSequence of bool [:X,Y:]; :: thesis: for p being set holds
( ex Fy being disjoint_valued FinSequence of bool X st
( dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Y-section ((F . n),p) ) ) & ex Fx being disjoint_valued FinSequence of bool Y st
( dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = X-section ((F . n),p) ) ) )
let p be set ; :: thesis: ( ex Fy being disjoint_valued FinSequence of bool X st
( dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Y-section ((F . n),p) ) ) & ex Fx being disjoint_valued FinSequence of bool Y st
( dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = X-section ((F . n),p) ) ) )
deffunc H₁( Nat) -> Subset of X = Y-section ((F . $1),p);
deffunc H₂( Nat) -> Subset of Y = X-section ((F . $1),p);
thus ex Fy being disjoint_valued FinSequence of bool X st
( dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Y-section ((F . n),p) ) ) :: thesis: ex Fx being disjoint_valued FinSequence of bool Y st
( dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = X-section ((F . n),p) ) )

proof

consider Fy being FinSequence of bool X such that
A3: ( len Fy = len F & ( for j being Nat st j in dom Fy holds
Fy . j = H₁(j) ) ) from FINSEQ_2:sch 1();
reconsider Fy = Fy as FinSequence of bool X ;

now :: thesis: for n, m being object st n <> m holds
Fy . n misses Fy . m

let n, m be object ; :: thesis: ( n <> m implies Fy . b₁ misses Fy . b₂ )
assume n <> m ; :: thesis: Fy . b₁ misses Fy . b₂
then A4: F . n misses F . m by PROB_2:def 2;

per cases ( ( n in dom Fy & m in dom Fy ) or not n in dom Fy or not m in dom Fy ) ;

suppose A5: ( n in dom Fy & m in dom Fy ) ; :: thesis: Fy . b₁ misses Fy . b₂

then reconsider n1 = n, m1 = m as Nat ;
( Fy . n = Y-section ((F . n1),p) & Fy . m = Y-section ((F . m1),p) ) by A3, A5;
hence Fy . n misses Fy . m by A4, Th29; :: thesis: verum

end;

suppose ( not n in dom Fy or not m in dom Fy ) ; :: thesis: Fy . b₁ misses Fy . b₂

then ( Fy . n = {} or Fy . m = {} ) by FUNCT_1:def 2;
hence Fy . n misses Fy . m ; :: thesis: verum

end;

end;

end;

then reconsider Fy = Fy as disjoint_valued FinSequence of bool X by PROB_2:def 2;
take Fy ; :: thesis: ( dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Y-section ((F . n),p) ) )
thus ( dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Y-section ((F . n),p) ) ) by A3, FINSEQ_3:29; :: thesis: verum

end;

thus ex Fx being disjoint_valued FinSequence of bool Y st
( dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = X-section ((F . n),p) ) ) :: thesis: verum

proof

consider Fx being FinSequence of bool Y such that
A3: ( len Fx = len F & ( for j being Nat st j in dom Fx holds
Fx . j = H₂(j) ) ) from FINSEQ_2:sch 1();
reconsider Fx = Fx as FinSequence of bool Y ;

now :: thesis: for n, m being object st n <> m holds
Fx . n misses Fx . m

let n, m be object ; :: thesis: ( n <> m implies Fx . b₁ misses Fx . b₂ )
assume n <> m ; :: thesis: Fx . b₁ misses Fx . b₂
then A4: F . n misses F . m by PROB_2:def 2;

per cases ( ( n in dom Fx & m in dom Fx ) or not n in dom Fx or not m in dom Fx ) ;

suppose A5: ( n in dom Fx & m in dom Fx ) ; :: thesis: Fx . b₁ misses Fx . b₂

then reconsider n1 = n, m1 = m as Nat ;
( Fx . n = X-section ((F . n1),p) & Fx . m = X-section ((F . m1),p) ) by A3, A5;
hence Fx . n misses Fx . m by A4, Th29; :: thesis: verum

end;

suppose ( not n in dom Fx or not m in dom Fx ) ; :: thesis: Fx . b₁ misses Fx . b₂

then ( Fx . n = {} or Fx . m = {} ) by FUNCT_1:def 2;
hence Fx . n misses Fx . m ; :: thesis: verum

end;

end;

end;

then reconsider Fx = Fx as disjoint_valued FinSequence of bool Y by PROB_2:def 2;
take Fx ; :: thesis: ( dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = X-section ((F . n),p) ) )
thus ( dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = X-section ((F . n),p) ) ) by A3, FINSEQ_3:29; :: thesis: verum

end;