let I be set ; :: thesis:
let f, g be ManySortedSet of I; :: thesis:
assume A1: f c= g ; :: thesis:
let x be object ; :: according to PBOOLE:def 2 :: thesis:
assume x in I * ; :: thesis:
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:
assume y in (f #) . x ; :: thesis:
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:

let x be object ; :: thesis:
assume x in dom (g * p) ; :: thesis:
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:

end;

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