let M be non empty set ; :: thesis: 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; :: thesis: 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; :: 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 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)} :: according to XBOOLE_0:def 10 :: thesis: Cl {(x . i)} c= pi ((Cl {x}),i)

proof

let a be object ; :: 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 Th29; :: thesis: verum

end;

reconsider f = f as Element of (product J) by A1;
let a be object ; :: 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 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)} ; :: thesis: 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

proof

let m be object ; :: 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 PRALG_1:def 15;

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:94;
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 TARSKI:def 1;
then (f +* (i .--> a)) . m = f . m by FUNCT_4:11;
hence (f +* (i .--> a)) . m in (Carrier J) . m by A4, A9, CARD_3:9; :: thesis: verum

end;

end;

end;

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)}

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:94; :: thesis: verum

end;

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

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

end;

end;

end;

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; :: thesis: verum