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
A1: dom s = I by PARTFUN1:def 2
.= dom f by PARTFUN1:def 2 ;
then for x being set st x in dom f holds
s . x in f . x by FUNCT_1:def 14;
hence s in product f by A1, Th18; :: thesis: verum