let I be set ; :: thesis: for A, B being ManySortedSet of I st A c= B holds
for f being FinSequence of I holds A * f c= B * f
let A, B be ManySortedSet of I; :: thesis: ( A c= B implies for f being FinSequence of I holds A * f c= B * f )
assume A1: A c= B ; :: thesis: for f being FinSequence of I holds A * f c= B * f
let f be FinSequence of I; :: thesis: A * f c= B * f
let j be object ; :: according to PBOOLE:def 2 :: thesis: ( not j in dom f or (A * f) . j c= (B * f) . j )
assume A2: j in dom f ; :: thesis: (A * f) . j c= (B * f) . j
then ( (A * f) . j = A . (f . j) & (B * f) . j = B . (f . j) ) by FUNCT_1:13;
hence (A * f) . j c= (B * f) . j by A1, A2, FUNCT_1:102; :: thesis: verum