let S be non empty functional set ; :: thesis: for i being set st i in dom (product" S) holds
(product" S) . i = { (f . i) where f is Element of S : verum }
let i be set ; :: thesis: ( i in dom (product" S) implies (product" S) . i = { (f . i) where f is Element of S : verum } )
assume A1: i in dom (product" S) ; :: thesis: (product" S) . i = { (f . i) where f is Element of S : verum }

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (f . i) where f is Element of S : verum } c= (product" S) . i

let x be object ; :: thesis: ( x in (product" S) . i implies x in { (f . i) where f is Element of S : verum } )
assume x in (product" S) . i ; :: thesis: x in { (f . i) where f is Element of S : verum }
then x in pi (S,i) by A1, Def12;
then ex f being Function st
( f in S & x = f . i ) by Def6;
hence x in { (f . i) where f is Element of S : verum } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . i) where f is Element of S : verum } or x in (product" S) . i )
assume x in { (f . i) where f is Element of S : verum } ; :: thesis: x in (product" S) . i
then ex f being Element of S st x = f . i ;
then x in pi (S,i) by Def6;
hence x in (product" S) . i by A1, Def12; :: thesis: verum