let I be set ; :: thesis: for f, g being ManySortedSet of I st f c= g holds
f # c= g #
let f, g be ManySortedSet of I; :: thesis: ( f c= g implies f # c= g # )
assume A1: f c= g ; :: thesis: f # c= g #
let x be object ; :: according to PBOOLE:def 2 :: thesis: ( not x in I * or (f #) . x c= (g #) . x )
assume x in I * ; :: thesis: (f #) . x c= (g #) . x
then reconsider p = x as Element of I * ;
A2: ( (f #) . p = product (f * p) & (g #) . p = product (g * p) ) by FINSEQ_2:def 5;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (f #) . x or y in (g #) . x )
assume y in (f #) . x ; :: thesis: y in (g #) . x
then consider h being Function such that
A3: ( y = h & dom h = dom (f * p) & ( for x being object st x in dom (f * p) holds
h . x in (f * p) . x ) ) by A2, CARD_3:def 5;
p is FinSequence of I by FINSEQ_1:def 11;
then A4: ( dom f = I & dom g = I & rng p c= I ) by PARTFUN1:def 2, FINSEQ_1:def 4;
then A5: ( dom (f * p) = dom p & dom (g * p) = dom p ) by RELAT_1:27;

now :: thesis: for x being object st x in dom (g * p) holds
h . x in (g * p) . x

let x be object ; :: thesis: ( x in dom (g * p) implies h . x in (g * p) . x )
assume x in dom (g * p) ; :: thesis: h . x in (g * p) . x
then A6: ( h . x in (f * p) . x & (f * p) . x = f . (p . x) & (g * p) . x = g . (p . x) & p . x in rng p ) by A3, A5, FUNCT_1:13, FUNCT_1:def 3;
then f . (p . x) c= g . (p . x) by A4, A1;
hence h . x in (g * p) . x by A6; :: thesis: verum

end;

hence y in (g #) . x by A2, A3, A5, CARD_3:9; :: thesis: verum