:: Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 1, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
theorem
:: ORDINAL3:1
for
X
being
set
holds
X
c=
succ
X
by
XBOOLE_1:7
;
theorem
:: ORDINAL3:2
for
X
,
Y
being
set
st
succ
X
c=
Y
holds
X
c=
Y
proof
end;
theorem
:: ORDINAL3:3
for
A
,
B
being
Ordinal
holds
(
A
in
B
iff
succ
A
in
succ
B
)
proof
end;
theorem
:: ORDINAL3:4
for
A
being
Ordinal
for
X
being
set
st
X
c=
A
holds
union
X
is
Ordinal
proof
end;
theorem
Th5
:
:: ORDINAL3:5
for
X
being
set
holds
union
(
On
X
)
is
Ordinal
proof
end;
theorem
Th6
:
:: ORDINAL3:6
for
A
being
Ordinal
for
X
being
set
st
X
c=
A
holds
On
X
=
X
proof
end;
theorem
Th7
:
:: ORDINAL3:7
for
A
being
Ordinal
holds
On
{
A
}
=
{
A
}
proof
end;
theorem
Th8
:
:: ORDINAL3:8
for
A
being
Ordinal
st
A
<>
{}
holds
{}
in
A
proof
end;
theorem
:: ORDINAL3:9
for
A
being
Ordinal
holds
inf
A
=
{}
proof
end;
theorem
:: ORDINAL3:10
for
A
being
Ordinal
holds
inf
{
A
}
=
A
proof
end;
theorem
:: ORDINAL3:11
for
A
being
Ordinal
for
X
being
set
st
X
c=
A
holds
meet
X
is
Ordinal
proof
end;
registration
let
A
,
B
be
Ordinal
;
cluster
A
\/
B
->
ordinal
;
coherence
A
\/
B
is
ordinal
proof
end;
cluster
A
/\
B
->
ordinal
;
coherence
A
/\
B
is
ordinal
proof
end;
end;
theorem
:: ORDINAL3:12
for
A
,
B
being
Ordinal
holds
(
A
\/
B
=
A
or
A
\/
B
=
B
)
proof
end;
theorem
:: ORDINAL3:13
for
A
,
B
being
Ordinal
holds
(
A
/\
B
=
A
or
A
/\
B
=
B
)
proof
end;
Lm1
:
1
=
succ
{}
;
theorem
Th14
:
:: ORDINAL3:14
for
A
being
Ordinal
st
A
in
1 holds
A
=
{}
proof
end;
theorem
:: ORDINAL3:15
1
=
{
{}
}
by
Lm1
;
theorem
Th16
:
:: ORDINAL3:16
for
A
being
Ordinal
holds
( not
A
c=
1 or
A
=
{}
or
A
=
1 )
proof
end;
theorem
:: ORDINAL3:17
for
A
,
B
,
C
,
D
being
Ordinal
st (
A
c=
B
or
A
in
B
) &
C
in
D
holds
A
+^
C
in
B
+^
D
proof
end;
theorem
:: ORDINAL3:18
for
A
,
B
,
C
,
D
being
Ordinal
st
A
c=
B
&
C
c=
D
holds
A
+^
C
c=
B
+^
D
proof
end;
theorem
Th19
:
:: ORDINAL3:19
for
A
,
B
,
C
,
D
being
Ordinal
st
A
in
B
& ( (
C
c=
D
&
D
<>
{}
) or
C
in
D
) holds
A
*^
C
in
B
*^
D
proof
end;
theorem
:: ORDINAL3:20
for
A
,
B
,
C
,
D
being
Ordinal
st
A
c=
B
&
C
c=
D
holds
A
*^
C
c=
B
*^
D
proof
end;
theorem
Th21
:
:: ORDINAL3:21
for
B
,
C
,
D
being
Ordinal
st
B
+^
C
=
B
+^
D
holds
C
=
D
proof
end;
theorem
Th22
:
:: ORDINAL3:22
for
B
,
C
,
D
being
Ordinal
st
B
+^
C
in
B
+^
D
holds
C
in
D
proof
end;
theorem
Th23
:
:: ORDINAL3:23
for
B
,
C
,
D
being
Ordinal
st
B
+^
C
c=
B
+^
D
holds
C
c=
D
proof
end;
theorem
Th24
:
:: ORDINAL3:24
for
A
,
B
being
Ordinal
holds
(
A
c=
A
+^
B
&
B
c=
A
+^
B
)
proof
end;
theorem
:: ORDINAL3:25
for
A
,
B
,
C
being
Ordinal
st
A
in
B
holds
(
A
in
B
+^
C
&
A
in
C
+^
B
)
proof
end;
theorem
Th26
:
:: ORDINAL3:26
for
A
,
B
being
Ordinal
st
A
+^
B
=
{}
holds
(
A
=
{}
&
B
=
{}
)
proof
end;
theorem
Th27
:
:: ORDINAL3:27
for
A
,
B
being
Ordinal
st
A
c=
B
holds
ex
C
being
Ordinal
st
B
=
A
+^
C
proof
end;
theorem
Th28
:
:: ORDINAL3:28
for
A
,
B
being
Ordinal
st
A
in
B
holds
ex
C
being
Ordinal
st
(
B
=
A
+^
C
&
C
<>
{}
)
proof
end;
theorem
Th29
:
:: ORDINAL3:29
for
A
,
B
being
Ordinal
st
A
<>
{}
&
A
is
limit_ordinal
holds
B
+^
A
is
limit_ordinal
proof
end;
theorem
Th30
:
:: ORDINAL3:30
for
A
,
B
,
C
being
Ordinal
holds
(
A
+^
B
)
+^
C
=
A
+^
(
B
+^
C
)
proof
end;
theorem
:: ORDINAL3:31
for
A
,
B
being
Ordinal
holds
( not
A
*^
B
=
{}
or
A
=
{}
or
B
=
{}
)
proof
end;
theorem
:: ORDINAL3:32
for
A
,
B
,
C
being
Ordinal
st
A
in
B
&
C
<>
{}
holds
(
A
in
B
*^
C
&
A
in
C
*^
B
)
proof
end;
theorem
Th33
:
:: ORDINAL3:33
for
B
,
A
,
C
being
Ordinal
st
B
*^
A
=
C
*^
A
&
A
<>
{}
holds
B
=
C
proof
end;
theorem
Th34
:
:: ORDINAL3:34
for
B
,
A
,
C
being
Ordinal
st
B
*^
A
in
C
*^
A
holds
B
in
C
proof
end;
theorem
Th35
:
:: ORDINAL3:35
for
B
,
A
,
C
being
Ordinal
st
B
*^
A
c=
C
*^
A
&
A
<>
{}
holds
B
c=
C
proof
end;
theorem
Th36
:
:: ORDINAL3:36
for
B
,
A
being
Ordinal
st
B
<>
{}
holds
(
A
c=
A
*^
B
&
A
c=
B
*^
A
)
proof
end;
theorem
:: ORDINAL3:37
for
A
,
B
being
Ordinal
st
A
*^
B
=
1 holds
(
A
=
1 &
B
=
1 )
proof
end;
theorem
Th38
:
:: ORDINAL3:38
for
A
,
B
,
C
being
Ordinal
holds
( not
A
in
B
+^
C
or
A
in
B
or ex
D
being
Ordinal
st
(
D
in
C
&
A
=
B
+^
D
) )
proof
end;
definition
let
C
be
Ordinal
;
let
fi
be
Ordinal-Sequence
;
func
C
+^
fi
->
Ordinal-Sequence
means
:
Def1
:
:: ORDINAL3:def 1
(
dom
it
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
it
.
A
=
C
+^
(
fi
.
A
)
) );
existence
ex
b
1
being
Ordinal-Sequence
st
(
dom
b
1
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
1
.
A
=
C
+^
(
fi
.
A
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Ordinal-Sequence
st
dom
b
1
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
1
.
A
=
C
+^
(
fi
.
A
)
) &
dom
b
2
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
2
.
A
=
C
+^
(
fi
.
A
)
) holds
b
1
=
b
2
proof
end;
func
fi
+^
C
->
Ordinal-Sequence
means
:: ORDINAL3:def 2
(
dom
it
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
it
.
A
=
(
fi
.
A
)
+^
C
) );
existence
ex
b
1
being
Ordinal-Sequence
st
(
dom
b
1
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
1
.
A
=
(
fi
.
A
)
+^
C
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Ordinal-Sequence
st
dom
b
1
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
1
.
A
=
(
fi
.
A
)
+^
C
) &
dom
b
2
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
2
.
A
=
(
fi
.
A
)
+^
C
) holds
b
1
=
b
2
proof
end;
func
C
*^
fi
->
Ordinal-Sequence
means
:: ORDINAL3:def 3
(
dom
it
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
it
.
A
=
C
*^
(
fi
.
A
)
) );
existence
ex
b
1
being
Ordinal-Sequence
st
(
dom
b
1
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
1
.
A
=
C
*^
(
fi
.
A
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Ordinal-Sequence
st
dom
b
1
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
1
.
A
=
C
*^
(
fi
.
A
)
) &
dom
b
2
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
2
.
A
=
C
*^
(
fi
.
A
)
) holds
b
1
=
b
2
proof
end;
func
fi
*^
C
->
Ordinal-Sequence
means
:
Def4
:
:: ORDINAL3:def 4
(
dom
it
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
it
.
A
=
(
fi
.
A
)
*^
C
) );
existence
ex
b
1
being
Ordinal-Sequence
st
(
dom
b
1
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
1
.
A
=
(
fi
.
A
)
*^
C
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Ordinal-Sequence
st
dom
b
1
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
1
.
A
=
(
fi
.
A
)
*^
C
) &
dom
b
2
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
2
.
A
=
(
fi
.
A
)
*^
C
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def1
defines
+^
ORDINAL3:def 1 :
for
C
being
Ordinal
for
fi
,
b
3
being
Ordinal-Sequence
holds
(
b
3
=
C
+^
fi
iff (
dom
b
3
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
3
.
A
=
C
+^
(
fi
.
A
)
) ) );
::
deftheorem
defines
+^
ORDINAL3:def 2 :
for
C
being
Ordinal
for
fi
,
b
3
being
Ordinal-Sequence
holds
(
b
3
=
fi
+^
C
iff (
dom
b
3
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
3
.
A
=
(
fi
.
A
)
+^
C
) ) );
::
deftheorem
defines
*^
ORDINAL3:def 3 :
for
C
being
Ordinal
for
fi
,
b
3
being
Ordinal-Sequence
holds
(
b
3
=
C
*^
fi
iff (
dom
b
3
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
3
.
A
=
C
*^
(
fi
.
A
)
) ) );
::
deftheorem
Def4
defines
*^
ORDINAL3:def 4 :
for
C
being
Ordinal
for
fi
,
b
3
being
Ordinal-Sequence
holds
(
b
3
=
fi
*^
C
iff (
dom
b
3
=
dom
fi
& ( for
A
being
Ordinal
st
A
in
dom
fi
holds
b
3
.
A
=
(
fi
.
A
)
*^
C
) ) );
theorem
Th39
:
:: ORDINAL3:39
for
fi
,
psi
being
Ordinal-Sequence
for
C
being
Ordinal
st
{}
<>
dom
fi
&
dom
fi
=
dom
psi
& ( for
A
,
B
being
Ordinal
st
A
in
dom
fi
&
B
=
fi
.
A
holds
psi
.
A
=
C
+^
B
) holds
sup
psi
=
C
+^
(
sup
fi
)
proof
end;
theorem
Th40
:
:: ORDINAL3:40
for
A
,
B
being
Ordinal
st
A
is
limit_ordinal
holds
A
*^
B
is
limit_ordinal
proof
end;
theorem
Th41
:
:: ORDINAL3:41
for
A
,
B
,
C
being
Ordinal
st
A
in
B
*^
C
&
B
is
limit_ordinal
holds
ex
D
being
Ordinal
st
(
D
in
B
&
A
in
D
*^
C
)
proof
end;
theorem
Th42
:
:: ORDINAL3:42
for
fi
,
psi
being
Ordinal-Sequence
for
C
being
Ordinal
st
dom
fi
=
dom
psi
&
C
<>
{}
&
sup
fi
is
limit_ordinal
& ( for
A
,
B
being
Ordinal
st
A
in
dom
fi
&
B
=
fi
.
A
holds
psi
.
A
=
B
*^
C
) holds
sup
psi
=
(
sup
fi
)
*^
C
proof
end;
theorem
Th43
:
:: ORDINAL3:43
for
fi
being
Ordinal-Sequence
for
C
being
Ordinal
st
{}
<>
dom
fi
holds
sup
(
C
+^
fi
)
=
C
+^
(
sup
fi
)
proof
end;
theorem
Th44
:
:: ORDINAL3:44
for
fi
being
Ordinal-Sequence
for
C
being
Ordinal
st
{}
<>
dom
fi
&
C
<>
{}
&
sup
fi
is
limit_ordinal
holds
sup
(
fi
*^
C
)
=
(
sup
fi
)
*^
C
proof
end;
theorem
Th45
:
:: ORDINAL3:45
for
B
,
A
being
Ordinal
st
B
<>
{}
holds
union
(
A
+^
B
)
=
A
+^
(
union
B
)
proof
end;
theorem
Th46
:
:: ORDINAL3:46
for
A
,
B
,
C
being
Ordinal
holds
(
A
+^
B
)
*^
C
=
(
A
*^
C
)
+^
(
B
*^
C
)
proof
end;
theorem
Th47
:
:: ORDINAL3:47
for
A
,
B
being
Ordinal
st
A
<>
{}
holds
ex
C
,
D
being
Ordinal
st
(
B
=
(
C
*^
A
)
+^
D
&
D
in
A
)
proof
end;
theorem
Th48
:
:: ORDINAL3:48
for
A
,
C1
,
D1
,
C2
,
D2
being
Ordinal
st
(
C1
*^
A
)
+^
D1
=
(
C2
*^
A
)
+^
D2
&
D1
in
A
&
D2
in
A
holds
(
C1
=
C2
&
D1
=
D2
)
proof
end;
theorem
Th49
:
:: ORDINAL3:49
for
B
,
A
being
Ordinal
st 1
in
B
&
A
<>
{}
&
A
is
limit_ordinal
holds
for
fi
being
Ordinal-Sequence
st
dom
fi
=
A
& ( for
C
being
Ordinal
st
C
in
A
holds
fi
.
C
=
C
*^
B
) holds
A
*^
B
=
sup
fi
proof
end;
theorem
:: ORDINAL3:50
for
A
,
B
,
C
being
Ordinal
holds
(
A
*^
B
)
*^
C
=
A
*^
(
B
*^
C
)
proof
end;
definition
let
A
,
B
be
Ordinal
;
func
A
-^
B
->
Ordinal
means
:
Def5
:
:: ORDINAL3:def 5
A
=
B
+^
it
if
B
c=
A
otherwise
it
=
{}
;
existence
( (
B
c=
A
implies ex
b
1
being
Ordinal
st
A
=
B
+^
b
1
) & ( not
B
c=
A
implies ex
b
1
being
Ordinal
st
b
1
=
{}
) )
by
Th27
;
uniqueness
for
b
1
,
b
2
being
Ordinal
holds
( (
B
c=
A
&
A
=
B
+^
b
1
&
A
=
B
+^
b
2
implies
b
1
=
b
2
) & ( not
B
c=
A
&
b
1
=
{}
&
b
2
=
{}
implies
b
1
=
b
2
) )
by
Th21
;
consistency
for
b
1
being
Ordinal
holds verum
;
func
A
div^
B
->
Ordinal
means
:
Def6
:
:: ORDINAL3:def 6
ex
C
being
Ordinal
st
(
A
=
(
it
*^
B
)
+^
C
&
C
in
B
)
if
B
<>
{}
otherwise
it
=
{}
;
consistency
for
b
1
being
Ordinal
holds verum
;
existence
( (
B
<>
{}
implies ex
b
1
,
C
being
Ordinal
st
(
A
=
(
b
1
*^
B
)
+^
C
&
C
in
B
) ) & ( not
B
<>
{}
implies ex
b
1
being
Ordinal
st
b
1
=
{}
) )
by
Th47
;
uniqueness
for
b
1
,
b
2
being
Ordinal
holds
( (
B
<>
{}
& ex
C
being
Ordinal
st
(
A
=
(
b
1
*^
B
)
+^
C
&
C
in
B
) & ex
C
being
Ordinal
st
(
A
=
(
b
2
*^
B
)
+^
C
&
C
in
B
) implies
b
1
=
b
2
) & ( not
B
<>
{}
&
b
1
=
{}
&
b
2
=
{}
implies
b
1
=
b
2
) )
by
Th48
;
end;
::
deftheorem
Def5
defines
-^
ORDINAL3:def 5 :
for
A
,
B
,
b
3
being
Ordinal
holds
( (
B
c=
A
implies (
b
3
=
A
-^
B
iff
A
=
B
+^
b
3
) ) & ( not
B
c=
A
implies (
b
3
=
A
-^
B
iff
b
3
=
{}
) ) );
::
deftheorem
Def6
defines
div^
ORDINAL3:def 6 :
for
A
,
B
,
b
3
being
Ordinal
holds
( (
B
<>
{}
implies (
b
3
=
A
div^
B
iff ex
C
being
Ordinal
st
(
A
=
(
b
3
*^
B
)
+^
C
&
C
in
B
) ) ) & ( not
B
<>
{}
implies (
b
3
=
A
div^
B
iff
b
3
=
{}
) ) );
definition
let
A
,
B
be
Ordinal
;
func
A
mod^
B
->
Ordinal
equals
:: ORDINAL3:def 7
A
-^
(
(
A
div^
B
)
*^
B
)
;
correctness
coherence
A
-^
(
(
A
div^
B
)
*^
B
)
is
Ordinal
;
;
end;
::
deftheorem
defines
mod^
ORDINAL3:def 7 :
for
A
,
B
being
Ordinal
holds
A
mod^
B
=
A
-^
(
(
A
div^
B
)
*^
B
)
;
theorem
:: ORDINAL3:51
for
A
,
B
being
Ordinal
st
A
in
B
holds
B
=
A
+^
(
B
-^
A
)
proof
end;
theorem
Th52
:
:: ORDINAL3:52
for
A
,
B
being
Ordinal
holds
(
A
+^
B
)
-^
A
=
B
proof
end;
theorem
Th53
:
:: ORDINAL3:53
for
A
,
B
,
C
being
Ordinal
st
A
in
B
& (
C
c=
A
or
C
in
A
) holds
A
-^
C
in
B
-^
C
proof
end;
theorem
Th54
:
:: ORDINAL3:54
for
A
being
Ordinal
holds
A
-^
A
=
{}
proof
end;
theorem
:: ORDINAL3:55
for
A
,
B
being
Ordinal
st
A
in
B
holds
(
B
-^
A
<>
{}
&
{}
in
B
-^
A
)
proof
end;
theorem
Th56
:
:: ORDINAL3:56
for
A
being
Ordinal
holds
(
A
-^
{}
=
A
&
{}
-^
A
=
{}
)
proof
end;
theorem
:: ORDINAL3:57
for
A
,
B
,
C
being
Ordinal
holds
A
-^
(
B
+^
C
)
=
(
A
-^
B
)
-^
C
proof
end;
theorem
:: ORDINAL3:58
for
A
,
B
,
C
being
Ordinal
st
A
c=
B
holds
C
-^
B
c=
C
-^
A
proof
end;
theorem
:: ORDINAL3:59
for
A
,
B
,
C
being
Ordinal
st
A
c=
B
holds
A
-^
C
c=
B
-^
C
proof
end;
theorem
:: ORDINAL3:60
for
C
,
A
,
B
being
Ordinal
st
C
<>
{}
&
A
in
B
+^
C
holds
A
-^
B
in
C
proof
end;
theorem
:: ORDINAL3:61
for
A
,
B
,
C
being
Ordinal
st
A
+^
B
in
C
holds
B
in
C
-^
A
proof
end;
theorem
:: ORDINAL3:62
for
A
,
B
being
Ordinal
holds
A
c=
B
+^
(
A
-^
B
)
proof
end;
theorem
:: ORDINAL3:63
for
A
,
C
,
B
being
Ordinal
holds
(
A
*^
C
)
-^
(
B
*^
C
)
=
(
A
-^
B
)
*^
C
proof
end;
theorem
Th64
:
:: ORDINAL3:64
for
A
,
B
being
Ordinal
holds
(
A
div^
B
)
*^
B
c=
A
proof
end;
theorem
Th65
:
:: ORDINAL3:65
for
A
,
B
being
Ordinal
holds
A
=
(
(
A
div^
B
)
*^
B
)
+^
(
A
mod^
B
)
proof
end;
theorem
:: ORDINAL3:66
for
A
,
B
,
C
,
D
being
Ordinal
st
A
=
(
B
*^
C
)
+^
D
&
D
in
C
holds
(
B
=
A
div^
C
&
D
=
A
mod^
C
)
proof
end;
theorem
:: ORDINAL3:67
for
A
,
B
,
C
being
Ordinal
st
A
in
B
*^
C
holds
(
A
div^
C
in
B
&
A
mod^
C
in
C
)
proof
end;
theorem
Th68
:
:: ORDINAL3:68
for
B
,
A
being
Ordinal
st
B
<>
{}
holds
(
A
*^
B
)
div^
B
=
A
proof
end;
theorem
:: ORDINAL3:69
for
A
,
B
being
Ordinal
holds
(
A
*^
B
)
mod^
B
=
{}
proof
end;
theorem
:: ORDINAL3:70
for
A
being
Ordinal
holds
(
{}
div^
A
=
{}
&
{}
mod^
A
=
{}
&
A
mod^
{}
=
A
)
proof
end;
theorem
:: ORDINAL3:71
for
A
being
Ordinal
holds
(
A
div^
1
=
A
&
A
mod^
1
=
{}
)
proof
end;
begin
:: from ZF_REFLE, 2007.03.13, A.T.
theorem
:: ORDINAL3:72
for
X
being
set
holds
sup
X
c=
succ
(
union
(
On
X
)
)
proof
end;
theorem
:: ORDINAL3:73
for
A
being
Ordinal
holds
succ
A
is_cofinal_with
1
proof
end;
:: from ARYTM_3, 2007.10.23, A.T.
theorem
Th74
:
:: ORDINAL3:74
for
a
,
b
being
Ordinal
st
a
+^
b
is
natural
holds
(
a
in
omega
&
b
in
omega
)
proof
end;
registration
let
a
,
b
be
natural
Ordinal
;
cluster
a
-^
b
->
natural
;
coherence
a
-^
b
is
natural
proof
end;
cluster
a
*^
b
->
natural
;
coherence
a
*^
b
is
natural
proof
end;
end;
theorem
:: ORDINAL3:75
for
a
,
b
being
Ordinal
st
a
*^
b
is
natural
& not
a
*^
b
is
empty
holds
(
a
in
omega
&
b
in
omega
)
proof
end;
definition
let
a
,
b
be
natural
Ordinal
;
:: original:
+^
redefine
func
a
+^
b
->
set
;
commutativity
for
a
,
b
being
natural
Ordinal
holds
a
+^
b
=
b
+^
a
proof
end;
end;
definition
let
a
,
b
be
natural
Ordinal
;
:: original:
*^
redefine
func
a
*^
b
->
set
;
commutativity
for
a
,
b
being
natural
Ordinal
holds
a
*^
b
=
b
*^
a
proof
end;
end;