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)) . b1 is plain
per cases ( x9 <> z or x9 = z ) ;
suppose A1: x9 <> z ; :: thesis: (canGFDistinction (F,z)) . b1 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;
end;
end;
hence canGFDistinction (F,z) is plain by GLIBPRE0:def 2; :: thesis: verum