let F be non empty Graph-yielding Function; :: thesis: for z being Element of dom F holds the_Vertices_of (canGFDistinction (F,z)) = (the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z)))
let z be Element of dom F; :: thesis: the_Vertices_of (canGFDistinction (F,z)) = (the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z)))
A1: dom (the_Vertices_of (canGFDistinction (F,z))) = dom (canGFDistinction (F,z)) by Def4
.= dom (canGFDistinction F) by FUNCT_7:30 ;
then A2: dom (the_Vertices_of (canGFDistinction (F,z))) = dom (the_Vertices_of (canGFDistinction F)) by Def4
.= dom ((the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z)))) by FUNCT_7:30 ;

now :: thesis: for x being object st x in dom (the_Vertices_of (canGFDistinction (F,z))) holds
(the_Vertices_of (canGFDistinction (F,z))) . x = ((the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z)))) . x

let x be object ; :: thesis: ( x in dom (the_Vertices_of (canGFDistinction (F,z))) implies (the_Vertices_of (canGFDistinction (F,z))) . b₁ = ((the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z)))) . b₁ )
assume x in dom (the_Vertices_of (canGFDistinction (F,z))) ; :: thesis: (the_Vertices_of (canGFDistinction (F,z))) . b₁ = ((the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z)))) . b₁
then reconsider x0 = x as Element of dom F by A1, Def25;

per cases ( x = z or x <> z ) ;

suppose A3: x = z ; :: thesis: (the_Vertices_of (canGFDistinction (F,z))) . b₁ = ((the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z)))) . b₁

z in dom F ;
then z in dom (canGFDistinction F) by Def25;
then A4: z in dom (the_Vertices_of (canGFDistinction F)) by Def4;
thus (the_Vertices_of (canGFDistinction (F,z))) . x = (the_Vertices_of F) . z by A3, Th97
.= the_Vertices_of (F . z) by Def8
.= ((the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z)))) . x by A3, A4, FUNCT_7:31 ; :: thesis: verum

end;

suppose A5: x <> z ; :: thesis: (the_Vertices_of (canGFDistinction (F,z))) . b₁ = ((the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z)))) . b₁

hence (the_Vertices_of (canGFDistinction (F,z))) . x = (the_Vertices_of (canGFDistinction F)) . x0 by Th98
.= ((the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z)))) . x by A5, FUNCT_7:32 ;
:: thesis: verum

end;

end;

end;

hence the_Vertices_of (canGFDistinction (F,z)) = (the_Vertices_of (canGFDistinction F)) +* (z,(the_Vertices_of (F . z))) by A2, FUNCT_1:2; :: thesis: verum