let X be non empty set ; :: thesis: for A1, A2 being Subset of X
for r1, r2 being Real holds <*(chi (r1,A1,X)),(chi (r2,A2,X))*> is summable FinSequence of Funcs (X,ExtREAL)
let A1, A2 be Subset of X; :: thesis: for r1, r2 being Real holds <*(chi (r1,A1,X)),(chi (r2,A2,X))*> is summable FinSequence of Funcs (X,ExtREAL)
let r1, r2 be Real; :: thesis: <*(chi (r1,A1,X)),(chi (r2,A2,X))*> is summable FinSequence of Funcs (X,ExtREAL)
reconsider f1 = chi (r1,A1,X), f2 = chi (r2,A2,X) as Element of Funcs (X,ExtREAL) by FUNCT_2:8;
reconsider F = <*f1,f2*> as FinSequence of Funcs (X,ExtREAL) ;
A1: ( f1 is V121() & f1 is V120() & f2 is V121() & f2 is V120() ) by Th4;
A2: dom F = {1,2} by FINSEQ_1:92;
now :: thesis: for n being Nat st n in dom F holds
F . n is without-infty
let n be Nat; :: thesis: ( n in dom F implies F . n is without-infty )
assume n in dom F ; :: thesis: F . n is without-infty
then ( n = 1 or n = 2 ) by A2, TARSKI:def 2;
hence F . n is without-infty by A1, FINSEQ_1:44; :: thesis: verum
end;
then F is without_-infty-valued ;
hence <*(chi (r1,A1,X)),(chi (r2,A2,X))*> is summable FinSequence of Funcs (X,ExtREAL) ; :: thesis: verum