consider u being Vector of M such that
A1: for p being Element of [: the carrier of M, the carrier of M:] holds
( p in u iff p `1 = p `2 ) by Th31;
u = { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 }
proof
for x being object holds
( x in u iff x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } )
proof
let x be object ; :: thesis: ( x in u iff x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } )
thus ( x in u implies x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } ) :: thesis: ( x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } implies x in u )
proof
assume A2: x in u ; :: thesis: x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 }
then reconsider r = x as Element of [: the carrier of M, the carrier of M:] ;
r `1 = r `2 by A1, A2;
hence x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } ; :: thesis: verum
end;
thus ( x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } implies x in u ) :: thesis: verum
proof
assume x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } ; :: thesis: x in u
then ex p being Element of [: the carrier of M, the carrier of M:] st
( x = p & p `1 = p `2 ) ;
hence x in u by A1; :: thesis: verum
end;
end;
hence u = { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } by TARSKI:2; :: thesis: verum
end;
hence { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } is Vector of M ; :: thesis: verum