let P, Q be non empty flat Poset; :: thesis: for K being non empty Chain of P
for f being Function of P,Q ex a being Element of P st
( ( K = {a} & f .: K = {(f . a)} ) or ( K = {(Bottom P),a} & f .: K = {(f . (Bottom P)),(f . a)} ) )
let K be non empty Chain of P; :: thesis: for f being Function of P,Q ex a being Element of P st
( ( K = {a} & f .: K = {(f . a)} ) or ( K = {(Bottom P),a} & f .: K = {(f . (Bottom P)),(f . a)} ) )
let f be Function of P,Q; :: thesis: ex a being Element of P st
( ( K = {a} & f .: K = {(f . a)} ) or ( K = {(Bottom P),a} & f .: K = {(f . (Bottom P)),(f . a)} ) )
consider a being Element of P such that
A1: ( K = {a} or K = {(Bottom P),a} ) by Thflat01;
take a ; :: thesis: ( ( K = {a} & f .: K = {(f . a)} ) or ( K = {(Bottom P),a} & f .: K = {(f . (Bottom P)),(f . a)} ) )
set z = Bottom P;
A3: the carrier of P = dom f by FUNCT_2:def 1;
( K = {a,a} or K = {(Bottom P),a} ) by A1, ENUMSET1:29;
then ( ( K = {a,a} & f .: K = {(f . a),(f . a)} ) or ( K = {(Bottom P),a} & f .: K = {(f . (Bottom P)),(f . a)} ) ) by A3, FUNCT_1:60;
hence ( ( K = {a} & f .: K = {(f . a)} ) or ( K = {(Bottom P),a} & f .: K = {(f . (Bottom P)),(f . a)} ) ) by ENUMSET1:29; :: thesis: verum