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 S1[ 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 H1( 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 & S1[x0,y] )
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) ;
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
; 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; verum