let S be non empty product-like set ; :: thesis: S = product (product" S)
thus S c= product (product" S) by Th94; :: according to XBOOLE_0:def 10 :: thesis: product (product" S) c= S
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (product" S) or x in S )
assume x in product (product" S) ; :: thesis: x in S
then consider g being Function such that
A1: x = g and
A2: dom g = dom (product" S) and
A3: for z being set st z in dom (product" S) holds
g . z in (product" S) . z by Def5;
consider p being Function such that
A4: S = product p by Def14;
set s = the Element of S;
A5: dom g = DOM S by A2, Th92
.= dom the Element of S by Def12
.= dom p by A4, Th18 ;
for z being set st z in dom p holds
g . z in p . z

proof

let z be set ; :: thesis: ( z in dom p implies g . z in p . z )
assume A6: z in dom p ; :: thesis: g . z in p . z
then g . z in (product" S) . z by A2, A3, A5;
then g . z in pi (S,z) by A2, A5, A6, Def13;
then ex f being Function st
( f in S & g . z = f . z ) by Def6;
hence g . z in p . z by A4, A6, Th18; :: thesis: verum

end;

hence x in S by A1, A4, A5, Th18; :: thesis: verum