let F be Function; :: thesis: for i being set st i in dom F holds
meet F c= F . i
let i be set ; :: thesis: ( i in dom F implies meet F c= F . i )
assume A1: i in dom F ; :: thesis: meet F c= F . i
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet F or x in F . i )
assume x in meet F ; :: thesis: x in F . i
hence x in F . i by A1, FUNCT_6:25, RELAT_1:38; :: thesis: verum