let X, Y be non empty set ; :: thesis: for F being disjoint_valued SetSequence of [:X,Y:]
for p being set holds
( ex Fy being disjoint_valued SetSequence of X st
for n being Nat holds Fy . n = Y-section ((F . n),p) & ex Fx being disjoint_valued SetSequence of Y st
for n being Nat holds Fx . n = X-section ((F . n),p) )
let F be disjoint_valued SetSequence of [:X,Y:]; :: thesis: for p being set holds
( ex Fy being disjoint_valued SetSequence of X st
for n being Nat holds Fy . n = Y-section ((F . n),p) & ex Fx being disjoint_valued SetSequence of Y st
for n being Nat holds Fx . n = X-section ((F . n),p) )
let p be set ; :: thesis: ( ex Fy being disjoint_valued SetSequence of X st
for n being Nat holds Fy . n = Y-section ((F . n),p) & ex Fx being disjoint_valued SetSequence of Y st
for n being Nat holds Fx . n = X-section ((F . n),p) )
thus ex Fy being disjoint_valued SetSequence of X st
for n being Nat holds Fy . n = Y-section ((F . n),p) :: thesis: ex Fx being disjoint_valued SetSequence of Y st
for n being Nat holds Fx . n = X-section ((F . n),p)

proof

deffunc H₁( Nat) -> Subset of X = Y-section ((F . $1),p);
consider Fy being SetSequence of X such that
A1: for n being Element of NAT holds Fy . n = H₁(n) from FUNCT_2:sch 4();

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

let n, m be Nat; :: thesis: ( n <> m implies Fy . n misses Fy . m )
A2: ( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;
assume n <> m ; :: thesis: Fy . n misses Fy . m
then F . n misses F . m by PROB_3:def 4;
then Y-section ((F . n),p) misses Y-section ((F . m),p) by Th29;
then Fy . n misses Y-section ((F . m),p) by A1, A2;
hence Fy . n misses Fy . m by A1, A2; :: thesis: verum

end;

then reconsider Fy = Fy as disjoint_valued SetSequence of X by PROB_3:def 4;
take Fy ; :: thesis: for n being Nat holds Fy . n = Y-section ((F . n),p)
let n be Nat; :: thesis: Fy . n = Y-section ((F . n),p)
n is Element of NAT by ORDINAL1:def 12;
hence Fy . n = Y-section ((F . n),p) by A1; :: thesis: verum

end;

deffunc H₁( Nat) -> Subset of Y = X-section ((F . $1),p);
consider Fx being SetSequence of Y such that
A3: for n being Element of NAT holds Fx . n = H₁(n) from FUNCT_2:sch 4();

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

let n, m be Nat; :: thesis: ( n <> m implies Fx . n misses Fx . m )
A4: ( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;
assume n <> m ; :: thesis: Fx . n misses Fx . m
then F . n misses F . m by PROB_3:def 4;
then X-section ((F . n),p) misses X-section ((F . m),p) by Th29;
then Fx . n misses X-section ((F . m),p) by A3, A4;
hence Fx . n misses Fx . m by A3, A4; :: thesis: verum

end;

then reconsider Fx = Fx as disjoint_valued SetSequence of Y by PROB_3:def 4;
take Fx ; :: thesis: for n being Nat holds Fx . n = X-section ((F . n),p)
let n be Nat; :: thesis: Fx . n = X-section ((F . n),p)
n is Element of NAT by ORDINAL1:def 12;
hence Fx . n = X-section ((F . n),p) by A3; :: thesis: verum