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: ( 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 ) implies IT1 = IT2 )
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: IT1 = IT2
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: IT1 . x = IT2 . x

per cases ( x = X or x <> X ) ;

suppose x = X ; :: thesis: IT1 . x = IT2 . x

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

end;

suppose C1: x <> X ; :: thesis: IT1 . x = IT2 . x

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

end;

end;

end;

hence IT1 = IT2 ; :: thesis: verum