let I be set ; for A, M being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st M in doms F holds
for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
let A, M be ManySortedSet of I; for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st M in doms F holds
for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
let B, C be V2() ManySortedSet of I; for F being ManySortedFunction of A,[|B,C|] st M in doms F holds
for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
let F be ManySortedFunction of A,[|B,C|]; ( M in doms F implies for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] )
assume A1:
M in doms F
; for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
let i be set ; ( i in I implies (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] )
assume A2:
i in I
; (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
then
M . i in (doms F) . i
by A1;
then A3:
M . i in dom (F . i)
by A2, MSSUBFAM:14;
A is_transformable_to [|B,C|]
;
then
M in A
by A1, MSSUBFAM:17;
then
F .. M in [|B,C|]
by CLOSURE1:3;
then
(F .. M) . i in [|B,C|] . i
by A2;
then
(F .. M) . i in [:(B . i),(C . i):]
by A2, PBOOLE:def 16;
then A4:
(F . i) . (M . i) in [:(B . i),(C . i):]
by A2, PRALG_1:def 20;
set z = (F . i) . (M . i);
(Mpr2 F) . i = pr2 (F . i)
by A2, Def2;
then A5: ((Mpr2 F) .. M) . i =
(pr2 (F . i)) . (M . i)
by A2, PRALG_1:def 20
.=
((F . i) . (M . i)) `2
by A3, MCART_1:def 13
;
(Mpr1 F) . i = pr1 (F . i)
by A2, Def1;
then ((Mpr1 F) .. M) . i =
(pr1 (F . i)) . (M . i)
by A2, PRALG_1:def 20
.=
((F . i) . (M . i)) `1
by A3, MCART_1:def 12
;
then
(F . i) . (M . i) = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
by A4, A5, MCART_1:21;
hence
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
by A2, PRALG_1:def 20; verum