let z, X be set ; :: thesis: ( z in product <%X%> implies ex x being set st
( x in X & z = <%x%> ) )
assume z in product <%X%> ; :: thesis: ex x being set st
( x in X & z = <%x%> )
then consider f being Function such that
A1: z = f and
A2: dom f = dom <%X%> and
A3: for x being object st x in dom <%X%> holds
f . x in <%X%> . x by CARD_3:def 5;
reconsider f = f as XFinSequence by A2, AFINSQ_1:5;
take f . 0 ; :: thesis: ( f . 0 in X & z = <%(f . 0)%> )
A4: 0 in {0} by TARSKI:def 1;
A5: <%X%> . 0 = X ;
len <%X%> = 1 by AFINSQ_1:34;
then len f = 1 by A2;
hence ( f . 0 in X & z = <%(f . 0)%> ) by A5, A4, A1, A2, A3, AFINSQ_1:34, CARD_1:49; :: thesis: verum