let M be non empty set ; :: thesis: for i being Element of M
for J being non-Empty TopSpace-yielding ManySortedSet of
for x being Point of (product J) holds pi (Cl {x}),i = Cl {(x . i)}
let i be Element of M; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
for x being Point of (product J) holds pi (Cl {x}),i = Cl {(x . i)}
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: thesis: for x being Point of (product J) holds pi (Cl {x}),i = Cl {(x . i)}
let x be Point of (product J); :: thesis: pi (Cl {x}),i = Cl {(x . i)}
thus pi (Cl {x}),i c= Cl {(x . i)} :: according to XBOOLE_0:def 10 :: thesis: Cl {(x . i)} c= pi (Cl {x}),i

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in pi (Cl {x}),i or a in Cl {(x . i)} )
assume a in pi (Cl {x}),i ; :: thesis: a in Cl {(x . i)}
then ex f being Function st
( f in Cl {x} & a = f . i ) by CARD_3:def 6;
hence a in Cl {(x . i)} by Th30; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Cl {(x . i)} or a in pi (Cl {x}),i )
assume A1: a in Cl {(x . i)} ; :: thesis: a in pi (Cl {x}),i
consider f being set such that
A2: f in Cl {x} by XBOOLE_0:def 1;
A3: f in the carrier of (product J) by A2;
reconsider f = f as Element of (product J) by A2;
set y = f +* (i .--> a);
A4: f in product (Carrier J) by A3, WAYBEL18:def 3;
A5: dom (Carrier J) = M by PARTFUN1:def 4;
then A6: dom f = M by A4, CARD_3:18;
A7: dom (f +* (i .--> a)) = (dom f) \/ (dom (i .--> a)) by FUNCT_4:def 1
.= M \/ {i} by A6, FUNCOP_1:19
.= M by ZFMISC_1:46 ;
A8: dom (i .--> a) = {i} by FUNCOP_1:19;
for m being set st m in dom (Carrier J) holds
(f +* (i .--> a)) . m in (Carrier J) . m

proof

let m be set ; :: thesis: ( m in dom (Carrier J) implies (f +* (i .--> a)) . m in (Carrier J) . m )
assume A9: m in dom (Carrier J) ; :: thesis: (f +* (i .--> a)) . m in (Carrier J) . m
then consider R being 1-sorted such that
A10: ( R = J . m & (Carrier J) . m = the carrier of R ) by A5, PRALG_1:def 13;

per cases ( m = i or m <> i ) ;

suppose A11: m = i ; :: thesis: (f +* (i .--> a)) . m in (Carrier J) . m

then (f +* (i .--> a)) . m = a by FUNCT_7:96;
hence (f +* (i .--> a)) . m in (Carrier J) . m by A1, A10, A11; :: thesis: verum

end;

suppose m <> i ; :: thesis: (f +* (i .--> a)) . m in (Carrier J) . m

then not m in dom (i .--> a) by A8, TARSKI:def 1;
then (f +* (i .--> a)) . m = f . m by FUNCT_4:12;
hence (f +* (i .--> a)) . m in (Carrier J) . m by A4, A9, CARD_3:18; :: thesis: verum

end;

end;

end;

then f +* (i .--> a) in product (Carrier J) by A5, A7, CARD_3:18;
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)}

proof

let m be Element of M; :: thesis: y . m in Cl {(x . m)}

per cases ( m = i or m <> i ) ;

suppose m = i ; :: thesis: y . m in Cl {(x . m)}

hence y . m in Cl {(x . m)} by A1, FUNCT_7:96; :: thesis: verum

end;

suppose m <> i ; :: thesis: y . m in Cl {(x . m)}

then not m in dom (i .--> a) by A8, TARSKI:def 1;
then y . m = f . m by FUNCT_4:12;
hence y . m in Cl {(x . m)} by A2, Th30; :: thesis: verum

end;

end;

end;

then A12: f +* (i .--> a) in Cl {x} by Th30;
(f +* (i .--> a)) . i = a by FUNCT_7:96;
hence a in pi (Cl {x}),i by A12, CARD_3:def 6; :: thesis: verum