let S be functional set ; :: thesis: for i being set st i in dom (product" S) holds
(product" S) . i = pi (S,i)
let i be set ; :: thesis: ( i in dom (product" S) implies (product" S) . i = pi (S,i) )

per cases ( S = {} or S <> {} ) ;

suppose S = {} ; :: thesis: ( i in dom (product" S) implies (product" S) . i = pi (S,i) )

then dom (product" S) = dom {} by Def13;
hence ( i in dom (product" S) implies (product" S) . i = pi (S,i) ) ; :: thesis: verum

end;

suppose A1: S <> {} ; :: thesis: ( i in dom (product" S) implies (product" S) . i = pi (S,i) )

assume i in dom (product" S) ; :: thesis: (product" S) . i = pi (S,i)
hence (product" S) . i = pi (S,i) by A1, Def13; :: thesis: verum

end;

end;