let I, a be set ; :: thesis: for A being ManySortedSet of
for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F
let A be ManySortedSet of ; :: 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 let i be
set ;
:: thesis: ( i in I implies (Mpr1 F) . i = (Mpr2 F) . i )assume A1:
i in I
;
:: thesis: (Mpr1 F) . i = (Mpr2 F) . ithen A2:
(Mpr1 F) . i = pr1 (F . i)
by Def1;
A3:
(Mpr2 F) . i = pr2 (F . i)
by A1, Def2;
A4:
dom (pr2 (F . i)) = dom (F . i)
by MCART_1:def 13;
now let y be
set ;
:: thesis: ( y in dom (F . i) implies (pr2 (F . i)) . y = ((F . i) . y) `1 )assume A5:
y in dom (F . i)
;
:: thesis: (pr2 (F . i)) . y = ((F . i) . y) `1 A6:
F . i is
Function of
(A . i),
([|(I --> {a}),(I --> {a})|] . i)
by A1, PBOOLE:def 18;
A7:
(F . i) . y in rng (F . i)
by A5, FUNCT_1:def 5;
rng (F . i) c= [|(I --> {a}),(I --> {a})|] . i
by A6, RELAT_1:def 19;
then A8:
rng (F . i) c= [:((I --> {a}) . i),((I --> {a}) . i):]
by A1, PBOOLE:def 21;
then
((F . i) . y) `1 in (I --> {a}) . i
by A7, MCART_1:10;
then A9:
((F . i) . y) `1 in {a}
by A1, FUNCOP_1:13;
((F . i) . y) `2 in (I --> {a}) . i
by A7, A8, MCART_1:10;
then A10:
((F . i) . y) `2 in {a}
by A1, FUNCOP_1:13;
thus (pr2 (F . i)) . y =
((F . i) . y) `2
by A5, MCART_1:def 13
.=
a
by A10, TARSKI:def 1
.=
((F . i) . y) `1
by A9, TARSKI:def 1
;
:: thesis: verum end; hence
(Mpr1 F) . i = (Mpr2 F) . i
by A2, A3, A4, MCART_1:def 12;
:: thesis: verum end;
hence
Mpr1 F = Mpr2 F
by PBOOLE:3; :: thesis: verum