let A, B be set ; :: thesis: for f being ManySortedSet of
for g being ManySortedSet of st f c= g holds
f # c= g #
let f be ManySortedSet of ; :: thesis: for g being ManySortedSet of st f c= g holds
f # c= g #
let g be ManySortedSet of ; :: thesis: ( f c= g implies f # c= g # )
assume A1:
f c= g
; :: thesis: f # c= g #
now let z be
set ;
:: thesis: ( z in f # implies z in g # )assume A2:
z in f #
;
:: thesis: z in g # then consider x,
y being
set such that A3:
[x,y] = z
by RELAT_1:def 1;
A4:
(
dom f = A &
dom g = B &
dom (f # ) = A * &
dom (g # ) = B * )
by PARTFUN1:def 4;
then reconsider x =
x as
Element of
A * by A2, A3, RELAT_1:def 4;
A5:
dom f c= dom g
by A1, RELAT_1:25;
rng x c= A
by FINSEQ_1:def 4;
then
rng x c= B
by A4, A5, XBOOLE_1:1;
then
x is
FinSequence of
B
by FINSEQ_1:def 4;
then reconsider x' =
x as
Element of
B * by FINSEQ_1:def 11;
A6:
(
rng x c= A &
rng x' c= B &
f tolerates g )
by A1, FINSEQ_1:def 4, PARTFUN1:135;
y =
(f # ) . x
by A2, A3, FUNCT_1:8
.=
product (f * x)
by PBOOLE:def 19
.=
product (g * x')
by A4, A6, Th2
.=
(g # ) . x'
by PBOOLE:def 19
;
hence
z in g #
by A3, A4, FUNCT_1:8;
:: thesis: verum end;
hence
f # c= g #
by TARSKI:def 3; :: thesis: verum