let a, b be real number ; 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:4, 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:18;
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, Th31
.=
1
by RVSUM_1:124
;
hence
a,b In_Power 0 = <*1*>
by A1, FINSEQ_1:57; verum