let x be object ; :: thesis: for X, Y being non empty set
for f being Function of X,Y st x in X holds
(Flatten f) . x in Y
let X, Y be non empty set ; :: thesis: for f being Function of X,Y st x in X holds
(Flatten f) . x in Y
let f be Function of X,Y; :: thesis: ( x in X implies (Flatten f) . x in Y )
assume A1: x in X ; :: thesis: (Flatten f) . x in Y
then reconsider xx = x as set ;
A2: not xx in xx ;
set FX = FlatPoset X;
reconsider x = x as Element of (FlatPoset X) by A1, XBOOLE_0:def 3;
f . x in Y by A1, FUNCT_2:5;
hence (Flatten f) . x in Y by DefFlatten04, A1, A2; :: thesis: verum