let I be non empty set ; :: thesis: for J being set
for A, B being ManySortedSet of I st A c= B holds
for f being Function of J,I holds A * f c= B * f
let J be set ; :: thesis: for A, B being ManySortedSet of I st A c= B holds
for f being Function of J,I holds A * f c= B * f
let A, B be ManySortedSet of I; :: thesis: ( A c= B implies for f being Function of J,I holds A * f c= B * f )
assume A1: A c= B ; :: thesis: for f being Function of J,I holds A * f c= B * f
let f be Function of J,I; :: thesis: A * f c= B * f
let j be object ; :: according to PBOOLE:def 2 :: thesis: ( not j in J or (A * f) . j c= (B * f) . j )
assume A2: j in J ; :: thesis: (A * f) . j c= (B * f) . j
then ( (A * f) . j = A . (f . j) & (B * f) . j = B . (f . j) ) by FUNCT_2:15;
hence (A * f) . j c= (B * f) . j by A1, A2, FUNCT_2:5; :: thesis: verum