let G be VGraph; :: thesis: for v1, v2, x being set st v1 <> v2 holds
(the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2
let v1, v2, x be set ; :: thesis: ( v1 <> v2 implies (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 )
set G2 = G .labelVertex (v1,x);
assume A1: v1 <> v2 ; :: thesis: (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2

now :: thesis: (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2

per cases ( v1 in the_Vertices_of G or not v1 in the_Vertices_of G ) ;

suppose A2: v1 in the_Vertices_of G ; :: thesis: (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2

not v2 in {v1} by A1, TARSKI:def 1;
then A3: not v2 in dom (v1 .--> x) ;
the_VLabel_of (G .labelVertex (v1,x)) = (the_VLabel_of G) +* (v1 .--> x) by A2, Th38;
hence (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 by A3, FUNCT_4:11; :: thesis: verum

end;

suppose not v1 in the_Vertices_of G ; :: thesis: (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2

hence (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 by Def22; :: thesis: verum

end;

end;

end;

hence (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 ; :: thesis: verum