let S be non empty product-like set ; :: thesis: S = product (product" S)
thus S c= product (product" S) by Th74; :: according to XBOOLE_0:def 10 :: thesis: product (product" S) c= S
let x be object ; :: 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 object 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 Def13;
set s = the Element of S;
A5: dom g = DOM S by A2, Def12
.= dom the Element of S by Lm2
.= dom p by A4, Th9 ;
for z being object st z in dom p holds
g . z in p . z

proof

let z be object ; :: 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, Def12;
then ex f being Function st
( f in S & g . z = f . z ) by Def6;
hence g . z in p . z by A4, A6, Th9; :: thesis: verum

end;

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