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 H₁( object ) -> set = Flatten (f,$1);
A5: for x being object st x in succ X holds
H₁(x) in succ Y

proof

let x be object ; :: thesis: ( x in succ X implies H₁(x) in succ Y )
assume x in succ X ; :: thesis: H₁(x) in succ Y

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

suppose B2: x in X ; :: thesis: H₁(x) in succ Y

then C1: H₁(x) = f . x by DefFlatten01;
f . x in Y by B2, FUNCT_2:5;
hence H₁(x) in succ Y by C1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x in X ; :: thesis: H₁(x) in succ Y

hence H₁(x) in succ Y by DefFlatten01, A401; :: thesis: verum

end;

end;

end;

ex h being Function of (succ X),(succ Y) st
for x being object st x in succ X holds
h . x = H₁(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 = H₁(x) ;
reconsider IT = IT as Function of (FlatPoset X),(FlatPoset Y) ;
A7: IT . X = H₁(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 = H₁(x) by A6
.= f . x by DefFlatten01, B1, B3, TARSKI:def 1 ;
hence IT . x = f . x ; :: thesis: verum

end;

hence ex b₁ being Function of (FlatPoset X),(FlatPoset Y) st
( b₁ . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
b₁ . x = f . x ) ) by A7; :: thesis: verum