dist (|[0,0]|,|[0,1]|) = sqrt (((0 - 0) ^2) + ((0 - 1) ^2)) by THYQ
.= sqrt ((0 * 0) + ((- 1) ^2)) by SQUARE_1:def 1
.= sqrt (0 + ((- 1) * (- 1))) by SQUARE_1:def 1
.= 1 by SQUARE_1:18 ;
hence dist (|[0,0]|,|[0,1]|) = 1 ; :: thesis: verum