let S1, S2 be set ; :: thesis: ( ( for f being object holds
( f in S1 iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) ) & ( for f being object holds
( f in S2 iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) ) implies S1 = S2 )
assume that
A12: for f being object holds
( f in S1 iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) and
A13: for f being object holds
( f in S2 iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) ; :: thesis: S1 = S2

now :: thesis: for x being object holds
( x in S1 iff x in S2 )

let x be object ; :: thesis: ( x in S1 iff x in S2 )
( x in S1 iff ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) ) by A12;
hence ( x in S1 iff x in S2 ) by A13; :: thesis: verum

end;

hence S1 = S2 by TARSKI:2; :: thesis: verum