let L be complete LATTICE; :: thesis: for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L
for f being set holds
( f is Element of product (doms F) iff f in dom (Frege F) )
let J be non empty set ; :: thesis: for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L
for f being set holds
( f is Element of product (doms F) iff f in dom (Frege F) )
let K be non-empty ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L
for f being set holds
( f is Element of product (doms F) iff f in dom (Frege F) )
let F be DoubleIndexedSet of K,L; :: thesis: for f being set holds
( f is Element of product (doms F) iff f in dom (Frege F) )
let f be set ; :: thesis: ( f is Element of product (doms F) iff f in dom (Frege F) )

hereby :: thesis: ( f in dom (Frege F) implies f is Element of product (doms F) )

assume f is Element of product (doms F) ; :: thesis: f in dom (Frege F)
then f in product (doms F) ;
hence f in dom (Frege F) by PARTFUN1:def 2; :: thesis: verum

end;

thus ( f in dom (Frege F) implies f is Element of product (doms F) ) ; :: thesis: verum