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 #
now A2:
dom f c= dom g
by A1, RELAT_1:25;
A3:
dom g = B
by PARTFUN1:def 4;
A4:
dom (g # ) = B *
by PARTFUN1:def 4;
let z be
set ;
( z in f # implies z in g # )A5:
dom f = A
by PARTFUN1:def 4;
assume A6:
z in f #
;
z in g # then consider x,
y being
set such that A7:
[x,y] = z
by RELAT_1:def 1;
dom (f # ) = A *
by PARTFUN1:def 4;
then reconsider x =
x as
Element of
A * by A6, A7, RELAT_1:def 4;
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, XBOOLE_1:1;
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:8
.=
product (f * x)
by PBOOLE:def 19
.=
product (g * x9)
by A1, A5, A3, A8, A9, Th2, PARTFUN1:135
.=
(g # ) . x9
by PBOOLE:def 19
;
hence
z in g #
by A7, A4, FUNCT_1:8;
verum end;
hence
f # c= g #
by TARSKI:def 3; verum