let S be functional with_common_domain set ; :: thesis: S c= product (product" S)
let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in S or f in product (product" S) )
assume A1: f in S ; :: thesis: f in product (product" S)
then reconsider f = f as Element of S ;
A2: dom f = DOM S by A1, Def12
.= dom (product" S) by Th92 ;
for i being set st i in dom (product" S) holds
f . i in (product" S) . i

proof

let i be set ; :: thesis: ( i in dom (product" S) implies f . i in (product" S) . i )
assume i in dom (product" S) ; :: thesis: f . i in (product" S) . i
then (product" S) . i = pi (S,i) by A1, Def13;
hence f . i in (product" S) . i by A1, Def6; :: thesis: verum

end;

hence f in product (product" S) by A2, Th18; :: thesis: verum