let I be non empty set ; 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 ; 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; ( A c= B implies for f being Function of J,I holds A * f c= B * f )
assume A1:
A c= B
; for f being Function of J,I holds A * f c= B * f
let f be Function of J,I; A * f c= B * f
let j be object ; PBOOLE:def 2 ( not j in J or (A * f) . j c= (B * f) . j )
assume A2:
j in J
; (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; verum