let S be functional with_common_domain set ; :: thesis: S c= product (product" S)
let f be object ; :: 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, Lm2
.= dom (product" S) by Def12 ;
for i being object st i in dom (product" S) holds
f . i in (product" S) . i
proof
let i be object ; :: 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 Def12;
hence f . i in (product" S) . i by A1, Def6; :: thesis: verum
end;
hence f in product (product" S) by A2, Th9; :: thesis: verum