set VL1 = S . (n + 1);
set VLN = S . n;
let IT1, IT2 be set ; :: thesis: ( ( n >= S .Lifespan() & IT1 = the Element of the_Vertices_of G & IT2 = the Element of the_Vertices_of G implies IT1 = IT2 ) & ( not n >= S .Lifespan() & not IT1 in dom (S . n) & S . (n + 1) = (S . n) +* (IT1 .--> ((S .Lifespan()) -' n)) & not IT2 in dom (S . n) & S . (n + 1) = (S . n) +* (IT2 .--> ((S .Lifespan()) -' n)) implies IT1 = IT2 ) )
thus ( n >= S .Lifespan() & IT1 = the Element of the_Vertices_of G & IT2 = the Element of the_Vertices_of G implies IT1 = IT2 ) ; :: thesis: ( not n >= S .Lifespan() & not IT1 in dom (S . n) & S . (n + 1) = (S . n) +* (IT1 .--> ((S .Lifespan()) -' n)) & not IT2 in dom (S . n) & S . (n + 1) = (S . n) +* (IT2 .--> ((S .Lifespan()) -' n)) implies IT1 = IT2 )
assume n < S .Lifespan() ; :: thesis: ( IT1 in dom (S . n) or not S . (n + 1) = (S . n) +* (IT1 .--> ((S .Lifespan()) -' n)) or IT2 in dom (S . n) or not S . (n + 1) = (S . n) +* (IT2 .--> ((S .Lifespan()) -' n)) or IT1 = IT2 )
assume that
A1: not IT1 in dom (S . n) and
A2: S . (n + 1) = (S . n) +* (IT1 .--> ((S .Lifespan()) -' n)) ; :: thesis: ( IT2 in dom (S . n) or not S . (n + 1) = (S . n) +* (IT2 .--> ((S .Lifespan()) -' n)) or IT1 = IT2 )
set f2 = IT2 .--> ((S .Lifespan()) -' n);
set f1 = IT1 .--> ((S .Lifespan()) -' n);
assume that
not IT2 in dom (S . n) and
A3: S . (n + 1) = (S . n) +* (IT2 .--> ((S .Lifespan()) -' n)) ; :: thesis: IT1 = IT2
dom (IT2 .--> ((S .Lifespan()) -' n)) = {IT2} ;
then A4: dom (S . (n + 1)) = (dom (S . n)) \/ {IT2} by A3, FUNCT_4:def 1;
dom (IT1 .--> ((S .Lifespan()) -' n)) = {IT1} ;
then A5: dom (S . (n + 1)) = (dom (S . n)) \/ {IT1} by A2, FUNCT_4:def 1;

now :: thesis: not IT1 <> IT2

assume IT1 <> IT2 ; :: thesis: contradiction
then not IT1 in {IT2} by TARSKI:def 1;
then A6: not IT1 in dom (S . (n + 1)) by A1, A4, XBOOLE_0:def 3;
IT1 in {IT1} by TARSKI:def 1;
hence contradiction by A5, A6, XBOOLE_0:def 3; :: thesis: verum

end;

hence IT1 = IT2 ; :: thesis: verum