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
meet F c= F . i

proof

let x be set ; :: 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:37, RELAT_1:60; :: thesis: verum

end;

hence meet F c= F . i ; :: thesis: verum