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 A201: X in succ 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;
deffunc H1( object ) -> set = Flatten (f,$1);
A5: for x being object st x in succ X holds
H1(x) in succ Y
proof
let x be object ; :: thesis: ( x in succ X implies H1(x) in succ Y )
assume x in succ X ; :: thesis: H1(x) in succ Y
per cases ( x in X or not x in X ) ;
end;
end;
ex h being Function of (succ X),(succ Y) st
for x being object st x in succ X holds
h . x = H1(x) from FUNCT_2:sch 2(A5);
 then consider IT being Function of (succ X),(succ Y) such that
A6: for x being object st x in succ X holds
IT . x = H1(x) ;
reconsider IT = IT as Function of (FlatPoset X),(FlatPoset Y) ;
A7: IT . X = H1(X) by A201, A6
.= Y by A0, DefFlatten01 ;
for x being Element of (FlatPoset X) st x <> X holds
IT . x = f . x
proof
let x be Element of (FlatPoset X); :: thesis: ( x <> X implies IT . x = f . x )
assume B1: x <> X ; :: thesis: IT . x = f . x
B3: ( x in {X} or x in X ) by XBOOLE_0:def 3;
IT . x = H1(x) by A6
.= f . x by DefFlatten01, B1, B3, TARSKI:def 1 ;
hence IT . x = f . x ; :: thesis: verum
end;
hence ex b1 being Function of (FlatPoset X),(FlatPoset Y) st
( b1 . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b1 . x = f . x ) ) by A7; :: thesis: verum