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

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