set z = X;
set r = Y;
A0: ( not X in X & not Y in Y ) ;
set FX = FlatPoset X;
set CX = succ X;
X in {X} by TARSKI:def 1;
then reconsider z = X as Element of (FlatPoset X) by XBOOLE_0:def 3;
set FY = FlatPoset Y;
set CY = succ Y;
Y in {Y} by TARSKI:def 1;
then A401: Y in succ Y by XBOOLE_0:def 3;
reconsider h1 = h1, h2 = h2 as continuous Function of (FlatPoset X),(FlatPoset Y) by A00;
defpred S₁[ object , object ] means for x being set
for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st x is Element of (FlatPoset X) & h1 = f1 & h2 = f2 & x = $1 holds
$2 = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D);
deffunc H₁( object ) -> set = BaseFunc02 ($1,(h1 . ((Flatten E1) . $1)),(h2 . ((Flatten E2) . $1)),I,J,D);
A5: for x0 being object st x0 in succ X holds
ex y being object st
( y in succ Y & S₁[x0,y] )

proof

let x0 be object ; :: thesis: ( x0 in succ X implies ex y being object st
( y in succ Y & S₁[x0,y] ) )
assume x0 in succ X ; :: thesis: ex y being object st
( y in succ Y & S₁[x0,y] )
set x1 = h1 . ((Flatten E1) . x0);
set x2 = h2 . ((Flatten E2) . x0);
set y = H₁(x0);
B200: S₁[x0,H₁(x0)] ;

per cases ( x0 in X or not x0 in X ) ;

suppose B2: x0 in X ; :: thesis: ex y being object st
( y in succ Y & S₁[x0,y] )

H₁(x0) in succ Y

proof

per cases ( ( h1 . ((Flatten E1) . x0) in Y & h2 . ((Flatten E2) . x0) in Y ) or not h1 . ((Flatten E1) . x0) in Y or not h2 . ((Flatten E2) . x0) in Y ) ;

suppose B3: ( h1 . ((Flatten E1) . x0) in Y & h2 . ((Flatten E2) . x0) in Y ) ; :: thesis: H₁(x0) in succ Y

then C0: [x0,(h1 . ((Flatten E1) . x0)),(h2 . ((Flatten E2) . x0))] in [:X,Y,Y:] by B2, MCART_1:69;

per cases ( x0 in D or not x0 in D ) ;

suppose x0 in D ; :: thesis: H₁(x0) in succ Y

then C01: H₁(x0) = I . x0 by DefBaseFunc02;
I . x0 in Y by B2, FUNCT_2:5;
hence H₁(x0) in succ Y by C01, XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x0 in D ; :: thesis: H₁(x0) in succ Y

then C01: H₁(x0) = J . [x0,(h1 . ((Flatten E1) . x0)),(h2 . ((Flatten E2) . x0))] by DefBaseFunc02, B2, B3;
J . [x0,(h1 . ((Flatten E1) . x0)),(h2 . ((Flatten E2) . x0))] in Y by C0, FUNCT_2:5;
hence H₁(x0) in succ Y by C01, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

suppose B3: ( not h1 . ((Flatten E1) . x0) in Y or not h2 . ((Flatten E2) . x0) in Y ) ; :: thesis: H₁(x0) in succ Y

per cases ( x0 in D or not x0 in D ) ;

suppose x0 in D ; :: thesis: H₁(x0) in succ Y

then C01: H₁(x0) = I . x0 by DefBaseFunc02;
I . x0 in Y by B2, FUNCT_2:5;
hence H₁(x0) in succ Y by C01, XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x0 in D ; :: thesis: H₁(x0) in succ Y

hence H₁(x0) in succ Y by A401, DefBaseFunc02, B3; :: thesis: verum

end;

end;

end;

end;

end;

hence ex y being object st
( y in succ Y & S₁[x0,y] ) by B200; :: thesis: verum

end;

suppose not x0 in X ; :: thesis: ex y being object st
( y in succ Y & S₁[x0,y] )

then ( not x0 in D & not ( x0 in X & h1 . ((Flatten E1) . x0) in Y & h2 . ((Flatten E2) . x0) in Y ) ) ;
then H₁(x0) = Y by DefBaseFunc02;
hence ex y being object st
( y in succ Y & S₁[x0,y] ) by A401, B200; :: thesis: verum

end;

end;

end;

consider IT being Function of (succ X),(succ Y) such that
A6: for x being object st x in succ X holds
S₁[x,IT . x] from FUNCT_2:sch 1(A5);
reconsider IT = IT as Function of (FlatPoset X),(FlatPoset Y) ;
A7: not z in D by A0;
A8: IT . z = BaseFunc02 (z,(h1 . ((Flatten E1) . z)),(h2 . ((Flatten E2) . z)),I,J,D) by A6
.= Y by A0, DefBaseFunc02, A7 ;
IT . (Bottom (FlatPoset X)) = Bottom (FlatPoset Y) by A8;
then reconsider IT = IT as continuous Function of (FlatPoset X),(FlatPoset Y) by Thflat07;
take IT ; :: thesis: for x being Element of (FlatPoset X)
for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
IT . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D)
thus for x being Element of (FlatPoset X)
for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
IT . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) by A6; :: thesis: verum