now :: thesis: for x9 being Element of dom (canGFDistinction (F,z)) holds (canGFDistinction (F,z)) . x9 is plain

let x9 be Element of dom (canGFDistinction (F,z)); :: thesis: (canGFDistinction (F,z)) . b₁ is plain

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

suppose A1: x9 <> z ; :: thesis: (canGFDistinction (F,z)) . b₁ is plain

x9 in dom (canGFDistinction (F,z)) ;
then x9 in dom F by Th94;
then reconsider x = x9 as Element of dom (canGFDistinction F) by Def25;
(canGFDistinction (F,z)) . x9 = (canGFDistinction F) . x by A1, FUNCT_7:32;
hence (canGFDistinction (F,z)) . x9 is plain ; :: thesis: verum

end;

suppose x9 = z ; :: thesis: (canGFDistinction (F,z)) . b₁ is plain

hence (canGFDistinction (F,z)) . x9 is plain by Th96; :: thesis: verum

end;

end;

end;

hence canGFDistinction (F,z) is plain by GLIBPRE0:def 2; :: thesis: verum