let x, X be set ; :: thesis: ( x in X implies <%x%> in product <%X%> )
set f = <%X%>;
set g = <%x%>;
assume A1: x in X ; :: thesis: <%x%> in product <%X%>
A2: len <%X%> = 1 by AFINSQ_1:34;
A3: len <%x%> = dom <%x%> ;
now :: thesis: for a being object st a in dom <%X%> holds
<%x%> . a in <%X%> . a
let a be object ; :: thesis: ( a in dom <%X%> implies <%x%> . a in <%X%> . a )
assume a in dom <%X%> ; :: thesis: <%x%> . a in <%X%> . a
then a = 0 by A2, CARD_1:49, TARSKI:def 1;
hence <%x%> . a in <%X%> . a by A1; :: thesis: verum
end;
hence <%x%> in product <%X%> by A2, A3, CARD_3:9, AFINSQ_1:34; :: thesis: verum