let M be MidSp; :: thesis: ex u being Vector of M st

for p being Element of [: the carrier of M, the carrier of M:] holds

( p in u iff p `1 = p `2 )

set a = the Element of M;

take [ the Element of M, the Element of M] ~ ; :: thesis: for p being Element of [: the carrier of M, the carrier of M:] holds

( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 )

let p be Element of [: the carrier of M, the carrier of M:]; :: thesis: ( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 )

( p `1 ,p `2 @@ the Element of M, the Element of M iff p ## [ the Element of M, the Element of M] ) ;

hence ( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 ) by Th13, Th26; :: thesis: verum

for p being Element of [: the carrier of M, the carrier of M:] holds

( p in u iff p `1 = p `2 )

set a = the Element of M;

take [ the Element of M, the Element of M] ~ ; :: thesis: for p being Element of [: the carrier of M, the carrier of M:] holds

( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 )

let p be Element of [: the carrier of M, the carrier of M:]; :: thesis: ( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 )

( p `1 ,p `2 @@ the Element of M, the Element of M iff p ## [ the Element of M, the Element of M] ) ;

hence ( p in [ the Element of M, the Element of M] ~ iff p `1 = p `2 ) by Th13, Th26; :: thesis: verum