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