let I be set ; :: thesis: for f being V8() ManySortedSet of I
for s being b₁ -compatible ManySortedSet of I holds s in product f
let f be V8() ManySortedSet of I; :: thesis: for s being f -compatible ManySortedSet of I holds s in product f
let s be f -compatible ManySortedSet of I; :: thesis: s in product f
A: dom s = I by PARTFUN1:def 4
.= dom f by PARTFUN1:def 4 ;
then for x being set st x in dom f holds
s . x in f . x by FUNCT_1:def 20;
hence s in product f by A, CARD_3:18; :: thesis: verum