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 without+infty & f1 is without-infty & f2 is without+infty & f2 is without-infty ) 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; :: 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