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 h = h as continuous Function of (FlatPoset X),(FlatPoset Y) by A00;
defpred S1[ object , object ] means for x being set
for f being continuous Function of (FlatPoset X),(FlatPoset Y) st x is Element of (FlatPoset X) & h = f & x = $1 holds
$2 = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D);
deffunc H1( object ) -> set = BaseFunc01 ($1,(h . ((Flatten E) . $1)),I,J,D);
A5: for x0 being object st x0 in succ X holds
ex y being object st
( y in succ Y & S1[x0,y] )
proof
let x0 be object ; :: thesis: ( x0 in succ X implies ex y being object st
( y in succ Y & S1[x0,y] ) )
assume x0 in succ X ; :: thesis: ex y being object st
( y in succ Y & S1[x0,y] )
set x1 = h . ((Flatten E) . x0);
set y = H1(x0);
B200: S1[x0,H1(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 & S1[x0,y] )
H1(x0) in succ Y
proof
per cases ( h . ((Flatten E) . x0) in Y or not h . ((Flatten E) . x0) in Y ) ;
end;
end;
hence ex y being object st
( y in succ Y & S1[x0,y] ) by B200; :: thesis: verum
end;
suppose not x0 in X ; :: thesis: ex y being object st
( y in succ Y & S1[x0,y] )
then ( not x0 in D & not ( x0 in X & h . ((Flatten E) . x0) in Y ) ) ;
then H1(x0) = Y by DefBaseFunc01;
hence ex y being object st
( y in succ Y & S1[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
S1[x,IT . x] from FUNCT_2:sch 1(A5);
 reconsider IT = IT as Function of (FlatPoset X),(FlatPoset Y) ;
A601: not z in D by A0;
A7: IT . z = BaseFunc01 (z,(h . ((Flatten E) . z)),I,J,D) by A6
.= Y by A0, DefBaseFunc01, A601 ;
IT . (Bottom (FlatPoset X)) = Bottom (FlatPoset Y) by A7;
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 f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds
IT . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D)
thus for x being Element of (FlatPoset X)
for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds
IT . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) by A6; :: thesis: verum