let I be set ; :: thesis: for A, M being ManySortedSet of
for B, C being V8() ManySortedSet of
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 ; :: thesis: for B, C being V8() ManySortedSet of
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 V8() ManySortedSet of ; :: thesis: 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|]; :: thesis: ( 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 ; :: thesis: for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
let i be set ; :: thesis: ( i in I implies (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] )
assume A2: i in I ; :: thesis: (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
then A3: (Mpr1 F) . i = pr1 (F . i) by Def1;
A4: (Mpr2 F) . i = pr2 (F . i) by A2, Def2;
A is_transformable_to [|B,C|]

proof

let i be set ; :: according to PZFMISC1:def 3 :: thesis: ( not i in I or not [|B,C|] . i = {} or A . i = {} )
assume i in I ; :: thesis: ( not [|B,C|] . i = {} or A . i = {} )
hence ( not [|B,C|] . i = {} or A . i = {} ) ; :: thesis: verum

end;

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, PBOOLE:def 4;
then (F .. M) . i in [:(B . i),(C . i):] by A2, PBOOLE:def 21;
then A5: (F . i) . (M . i) in [:(B . i),(C . i):] by A2, PRALG_1:def 18;
set z = (F . i) . (M . i);
M . i in (doms F) . i by A1, A2, PBOOLE:def 4;
then A6: M . i in dom (F . i) by A2, MSSUBFAM:14;
A7: ((Mpr1 F) .. M) . i = (pr1 (F . i)) . (M . i) by A2, A3, PRALG_1:def 18
.= ((F . i) . (M . i)) `1 by A6, MCART_1:def 12 ;
((Mpr2 F) .. M) . i = (pr2 (F . i)) . (M . i) by A2, A4, PRALG_1:def 18
.= ((F . i) . (M . i)) `2 by A6, MCART_1:def 13 ;
then (F . i) . (M . i) = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] by A5, A7, MCART_1:23;
hence (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] by A2, PRALG_1:def 18; :: thesis: verum