let M be non empty set ; :: thesis: for i being Element of M
for J being non-Empty TopSpace-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; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of M
for x being Point of (product J) holds pi (Cl {x}),i = Cl {(x . i)}
let J be non-Empty TopSpace-yielding ManySortedSet of M; :: 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)}
consider f being set 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)} :: 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;

reconsider f = f as Element of (product J) by A1;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( 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 4;
A4: f in product (Carrier J) by A2, WAYBEL18:def 3;
then A5: dom f = M by A3, CARD_3:18;
A6: dom (i .--> a) = {i} by FUNCOP_1:19;
assume A7: a in Cl {(x . i)} ; :: thesis: a in pi (Cl {x}),i
A8: 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 A10: ex R being 1-sorted st
( R = J . m & (Carrier J) . m = the carrier of R ) by A3, 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 A7, 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 A6, 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;

dom (f +* (i .--> a)) = (dom f) \/ (dom (i .--> a)) by FUNCT_4:def 1
.= M \/ {i} by A5, FUNCOP_1:19
.= M by ZFMISC_1:46 ;
then f +* (i .--> a) in product (Carrier J) by A3, A8, 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 A7, FUNCT_7:96; :: thesis: verum

end;

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

then not m in dom (i .--> a) by A6, TARSKI:def 1;
then y . m = f . m by FUNCT_4:12;
hence y . m in Cl {(x . m)} by A1, 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