let I be set ; :: thesis: for A, M being ManySortedSet of I
for B, C being non-empty 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; :: thesis: for B, C being non-empty 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 non-empty ManySortedSet of I; :: 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 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; :: thesis: verum