(
op2
is
Function
of
[:
1,1
:]
,1 & 1
c=
REAL
)
by
CARD_1:49
,
ZFMISC_1:31
,
Lm1
;
hence
Empty^2-to-zero
is
Function
of
[:
1,1
:]
,
REAL
by
FUNCT_2:7
;
:: thesis:
verum