let a, b be real number ; :: thesis: 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 ) ;
A4: 1 in dom (a,b In_Power 0 ) by A2, TARSKI:def 1;
reconsider i = i as Element of NAT by A3;
A5: 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 A5;
(a,b In_Power 0 ) . 1 = ((0 choose 0 ) * (a |^ l1)) * (b |^ m1) by A4, A5, Def4
.= (1 * (a |^ 0 )) * (b |^ 0 ) by A5, Th31
.= (1 * 1) * (b |^ 0 ) by RVSUM_1:124
.= 1 by RVSUM_1:124 ;
hence a,b In_Power 0 = <*1*> by A1, FINSEQ_1:57; :: thesis: verum