let I be set ; :: thesis: for f being non-empty ManySortedSet of I
for s being b₁ -compatible ManySortedSet of I holds s in product f
let f be non-empty 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 object st x in dom f holds
s . x in f . x by FUNCT_1:def 14;
hence s in product f by A1, Th9; :: thesis: verum