let M be non empty set ; for i being Element of M
for J being non-Empty TopStruct-yielding ManySortedSet of M
for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}
let i be Element of M; for J being non-Empty TopStruct-yielding ManySortedSet of M
for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}
let J be non-Empty TopStruct-yielding ManySortedSet of M; for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}
let x be Point of (product J); pi ((Cl {x}),i) = Cl {(x . i)}
consider f being object such that
A1:
f in Cl {x}
by XBOOLE_0:def 1;
A2:
f in the carrier of (product J)
by A1;
thus
pi ((Cl {x}),i) c= Cl {(x . i)}
XBOOLE_0:def 10 Cl {(x . i)} c= pi ((Cl {x}),i)
reconsider f = f as Element of (product J) by A1;
let a be object ; TARSKI:def 3 ( not a in Cl {(x . i)} or a in pi ((Cl {x}),i) )
set y = f +* (i .--> a);
A3:
dom (Carrier J) = M
by PARTFUN1:def 2;
A4:
f in product (Carrier J)
by A2, WAYBEL18:def 3;
then A5:
dom f = M
by A3, CARD_3:9;
assume A7:
a in Cl {(x . i)}
; a in pi ((Cl {x}),i)
A8:
for m being object st m in dom (Carrier J) holds
(f +* (i .--> a)) . m in (Carrier J) . m
dom (f +* (i .--> a)) =
(dom f) \/ (dom (i .--> a))
by FUNCT_4:def 1
.=
M \/ {i}
by A5
.=
M
by ZFMISC_1:40
;
then
f +* (i .--> a) in product (Carrier J)
by A3, A8, CARD_3:9;
then reconsider y = f +* (i .--> a) as Element of (product J) by WAYBEL18:def 3;
for m being Element of M holds y . m in Cl {(x . m)}
then A12:
f +* (i .--> a) in Cl {x}
by Th29;
(f +* (i .--> a)) . i = a
by FUNCT_7:94;
hence
a in pi ((Cl {x}),i)
by A12, CARD_3:def 6; verum