let L be complete LATTICE; :: thesis: for J being non empty set

for K being V9() 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 V9() 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 V9() 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) )

for K being V9() 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 V9() 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 V9() 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) )

thus
( f in dom (Frege F) implies f is Element of product (doms F) )
; :: thesis: verumassume
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;then f in product (doms F) ;

hence f in dom (Frege F) by PARTFUN1:def 2; :: thesis: verum