let IT1, IT2 be set ; :: thesis: ( ( n >= S .Lifespan() & IT1 = choose (the_Vertices_of G) & IT2 = choose (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 = choose (the_Vertices_of G) & IT2 = choose (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 )
set VLN = S . n;
set VL1 = S . (n + 1);
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 A3: ( not IT1 in dom (S . n) & 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 )
assume A4: ( not IT2 in dom (S . n) & S . (n + 1) = (S . n) +* (IT2 .--> ((S .Lifespan() ) -' n)) ) ; :: thesis: IT1 = IT2
set f1 = IT1 .--> ((S .Lifespan() ) -' n);
set f2 = IT2 .--> ((S .Lifespan() ) -' n);
A5: ( dom (IT1 .--> ((S .Lifespan() ) -' n)) = {IT1} & rng (IT1 .--> ((S .Lifespan() ) -' n)) = {((S .Lifespan() ) -' n)} ) by FUNCOP_1:14, FUNCOP_1:19;
A6: ( dom (IT2 .--> ((S .Lifespan() ) -' n)) = {IT2} & rng (IT2 .--> ((S .Lifespan() ) -' n)) = {((S .Lifespan() ) -' n)} ) by FUNCOP_1:14, FUNCOP_1:19;
A7: dom (S . (n + 1)) = (dom (S . n)) \/ {IT1} by A3, A5, FUNCT_4:def 1;
A8: dom (S . (n + 1)) = (dom (S . n)) \/ {IT2} by A4, A6, FUNCT_4:def 1;

now

assume IT1 <> IT2 ; :: thesis: contradiction
then not IT1 in {IT2} by TARSKI:def 1;
then A9: not IT1 in dom (S . (n + 1)) by A3, A8, XBOOLE_0:def 3;
IT1 in {IT1} by TARSKI:def 1;
hence contradiction by A7, A9, XBOOLE_0:def 3; :: thesis: verum

end;

hence IT1 = IT2 ; :: thesis: verum