let a, b be Real; (a,b) In_Power 0 = <*1*>
set F = (a,b) In_Power 0;
A1: len ((a,b) In_Power 0) =
0 + 1
by Def4
.=
1
;
then A2:
dom ((a,b) In_Power 0) = {1}
by FINSEQ_1:2, FINSEQ_1:def 3;
then
1 in dom ((a,b) In_Power 0)
by TARSKI:def 1;
then consider i being set such that
A3:
i in dom ((a,b) In_Power 0)
;
reconsider i = i as Element of NAT by A3;
A4:
i = 1
by A2, A3, TARSKI:def 1;
then reconsider m1 = i - 1 as Element of NAT by INT_1:5;
reconsider l1 = 0 - m1 as Element of NAT by A4;
1 in dom ((a,b) In_Power 0)
by A2, TARSKI:def 1;
then ((a,b) In_Power 0) . 1 =
((0 choose 0) * (a |^ l1)) * (b |^ m1)
by A4, Def4
.=
(1 * (a |^ 0)) * (b |^ 0)
by A4, Th21
.=
1
by RVSUM_1:94
;
hence
(a,b) In_Power 0 = <*1*>
by A1, FINSEQ_1:40; verum