deffunc H₁( Nat) -> Element of REAL = In (((f . ((tagged_of TD) . $1)) * (vol (divset ((division_of TD),$1)))),REAL);
consider IT being FinSequence of REAL such that
A1: ( len IT = len (division_of TD) & ( for i being Nat st i in dom IT holds
IT . i = H₁(i) ) ) from FINSEQ_2:sch 1();
take IT ; :: thesis: ( len IT = len TD & ( for i being Nat st i in dom TD holds
IT . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) )
thus len IT = len TD by A1; :: thesis: for i being Nat st i in dom TD holds
IT . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))
let i be Nat; :: thesis: ( i in dom TD implies IT . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) )
A2: H₁(i) = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ;
assume i in dom TD ; :: thesis: IT . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))
then i in Seg (len (division_of TD)) by FINSEQ_1:def 3;
then i in dom IT by A1, FINSEQ_1:def 3;
hence IT . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) by A1, A2; :: thesis: verum