set FX = FlatPoset X;
set FY = FlatPoset Y;
set CX = succ X;
set CY = succ Y;
let IT1, IT2 be Function of (FlatPoset X),(FlatPoset Y); :: thesis:
assume B1: ( IT1 . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
IT1 . x = f . x ) & IT2 . X = Y & ( for x being Element of (FlatPoset X) st x <> X holds
IT2 . x = f . x ) ) ; :: thesis:
reconsider IT1 = IT1, IT2 = IT2 as Function of (succ X),(succ Y) ;
for x being Element of succ X holds IT1 . x = IT2 . x

proof

let x be Element of succ X; :: thesis:

per cases ;

suppose x = X ; :: thesis:

hence IT1 . x = IT2 . x by B1; :: thesis:

end;

suppose C1: x <> X ; :: thesis:

then IT1 . x = f . x by B1
.= IT2 . x by C1, B1 ;
hence IT1 . x = IT2 . x ; :: thesis:

end;

end;

end;

hence IT1 = IT2 ; :: thesis: