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

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