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 x be object ; :: according to PBOOLE:def 2 :: thesis: ( not x in J or (A * f) . x c= (B * f) . x )
assume A2: x in J ; :: thesis: (A * f) . x c= (B * f) . x
then reconsider i = f . x as Element of I by FUNCT_2:5;
( (A * f) . x = A . i & (B * f) . x = B . i ) by A2, FUNCT_2:15;
hence (A * f) . x c= (B * f) . x by A1; :: thesis: verum