let a, I be set ; :: thesis: for A being ManySortedSet of I
for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F
let A be ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F
let F be ManySortedFunction of A,[|(I --> {a}),(I --> {a})|]; :: thesis: Mpr1 F = Mpr2 F

now :: thesis: for i being object st i in I holds
(Mpr1 F) . i = (Mpr2 F) . i

let i be object ; :: thesis: ( i in I implies (Mpr1 F) . i = (Mpr2 F) . i )
A1: dom (pr2 (F . i)) = dom (F . i) by MCART_1:def 13;
assume A2: i in I ; :: thesis: (Mpr1 F) . i = (Mpr2 F) . i

A3: now :: thesis: for y being object st y in dom (F . i) holds
(pr2 (F . i)) . y = ((F . i) . y) `1

let y be object ; :: thesis: ( y in dom (F . i) implies (pr2 (F . i)) . y = ((F . i) . y) `1 )
assume A4: y in dom (F . i) ; :: thesis: (pr2 (F . i)) . y = ((F . i) . y) `1
A5: (F . i) . y in rng (F . i) by A4, FUNCT_1:def 3;
F . i is Function of (A . i),([|(I --> {a}),(I --> {a})|] . i) by A2, PBOOLE:def 15;
then rng (F . i) c= [|(I --> {a}),(I --> {a})|] . i by RELAT_1:def 19;
then A6: rng (F . i) c= [:((I --> {a}) . i),((I --> {a}) . i):] by A2, PBOOLE:def 16;
then ((F . i) . y) `1 in (I --> {a}) . i by A5, MCART_1:10;
then A7: ((F . i) . y) `1 in {a} by A2, FUNCOP_1:7;
((F . i) . y) `2 in (I --> {a}) . i by A5, A6, MCART_1:10;
then A8: ((F . i) . y) `2 in {a} by A2, FUNCOP_1:7;
thus (pr2 (F . i)) . y = ((F . i) . y) `2 by A4, MCART_1:def 13
.= a by A8, TARSKI:def 1
.= ((F . i) . y) `1 by A7, TARSKI:def 1 ; :: thesis: verum

end;

( (Mpr1 F) . i = pr1 (F . i) & (Mpr2 F) . i = pr2 (F . i) ) by A2, Def1, Def2;
hence (Mpr1 F) . i = (Mpr2 F) . i by A1, A3, MCART_1:def 12; :: thesis: verum

end;

hence Mpr1 F = Mpr2 F ; :: thesis: verum