let J, D be set ; :: thesis: for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) )
let K be ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) )
let F be DoubleIndexedSet of K,D; :: thesis: for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) )
let f be Function; :: thesis: ( f in dom (Frege F) implies for j being set st j in J holds
( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) )
assume A1: f in dom (Frege F) ; :: thesis: for j being set st j in J holds
( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) )
let j be set ; :: thesis: ( j in J implies ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) ) )
assume j in J ; :: thesis: ( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) )
then A2: j in dom F by PARTFUN1:def 2;
hence ((Frege F) . f) . j = (F . j) . (f . j) by A1, Th9; :: thesis: (F . j) . (f . j) in rng ((Frege F) . f)
thus (F . j) . (f . j) in rng ((Frege F) . f) by A1, A2, Th9; :: thesis: verum