set bTS = _bool TS;
set wTS = the carrier of (_bool TS);
set tTS = the Tran of (_bool TS);
for x, y1, y2 being object st [x,y1] in the Tran of (_bool TS) & [x,y2] in the Tran of (_bool TS) holds
y1 = y2
proof
let x,
y1,
y2 be
object ;
( [x,y1] in the Tran of (_bool TS) & [x,y2] in the Tran of (_bool TS) implies y1 = y2 )
assume that A1:
[x,y1] in the
Tran of
(_bool TS)
and A2:
[x,y2] in the
Tran of
(_bool TS)
;
y1 = y2
reconsider x =
x as
Element of
[: the carrier of (_bool TS),(Lex E):] by A1, ZFMISC_1:87;
reconsider y1 =
y1,
y2 =
y2 as
Element of the
carrier of
(_bool TS) by A1, A2, ZFMISC_1:87;
the
carrier of
(_bool TS) = bool the
carrier of
TS
by Def1;
then consider xc,
xi being
object such that A3:
xc in the
carrier of
(_bool TS)
and A4:
xi in Lex E
and A5:
x = [xc,xi]
by ZFMISC_1:def 2;
reconsider xc =
xc as
Element of the
carrier of
(_bool TS) by A3;
reconsider xi =
xi as
Element of
Lex E by A4;
reconsider xi =
xi as
Element of
E ^omega ;
reconsider xc =
xc,
y1 =
y1,
y2 =
y2 as
Subset of
TS by Def1;
(
y1 = xi -succ_of (
xc,
TS) &
y2 = xi -succ_of (
xc,
TS) )
by A1, A2, A5, Def1;
hence
y1 = y2
;
verum
end;
then A6:
the Tran of (_bool TS) is Function
by FUNCT_1:def 1;
the carrier of (_bool TS) = bool the carrier of TS
by Def1;
hence
( not _bool TS is empty & _bool TS is deterministic )
by A6, Th11; verum