( 1 in INT & 0 in INT ) by INT_1:def 2;
then reconsider s = [1,0] as Element of [:INT,INT:] by ZFMISC_1:87;
take s ; :: thesis: ((s `1) ^2) - (D * ((s `2) ^2)) = 1
thus ((s `1) ^2) - (D * ((s `2) ^2)) = 1 ; :: thesis: verum