let A, B be set ; for f being ManySortedSet of A
for g being ManySortedSet of B st f c= g holds
f # c= g #
let f be ManySortedSet of A; for g being ManySortedSet of B st f c= g holds
f # c= g #
let g be ManySortedSet of B; ( f c= g implies f # c= g # )
assume A1:
f c= g
; f # c= g #
A2:
dom f c= dom g
by A1, RELAT_1:11;
A3:
dom g = B
by PARTFUN1:def 2;
A4:
dom (g #) = B *
by PARTFUN1:def 2;
let z be object ; TARSKI:def 3 ( not z in f # or z in g # )
A5:
dom f = A
by PARTFUN1:def 2;
assume A6:
z in f #
; z in g #
then consider x, y being object such that
A7:
[x,y] = z
by RELAT_1:def 1;
dom (f #) = A *
by PARTFUN1:def 2;
then reconsider x = x as Element of A * by A6, A7, XTUPLE_0:def 12;
A8:
rng x c= A
by FINSEQ_1:def 4;
rng x c= A
by FINSEQ_1:def 4;
then
rng x c= B
by A5, A3, A2;
then
x is FinSequence of B
by FINSEQ_1:def 4;
then reconsider x9 = x as Element of B * by FINSEQ_1:def 11;
A9:
rng x9 c= B
by FINSEQ_1:def 4;
y =
(f #) . x
by A6, A7, FUNCT_1:1
.=
product (f * x)
by FINSEQ_2:def 5
.=
product (g * x9)
by A1, A5, A3, A8, A9, PARTFUN1:54, PARTFUN1:79
.=
(g #) . x9
by FINSEQ_2:def 5
;
hence
z in g #
by A7, A4, FUNCT_1:1; verum