let X be set ; :: thesis: for B being disjoint_valued FinSequence of bool X
for a being object st a in X holds
( (arity-from-list B) . a <> 0 iff ex n being Nat st a in B . n )
let B be disjoint_valued FinSequence of bool X; :: thesis: for a being object st a in X holds
( (arity-from-list B) . a <> 0 iff ex n being Nat st a in B . n )
let a be object ; :: thesis: ( a in X implies ( (arity-from-list B) . a <> 0 iff ex n being Nat st a in B . n ) )
assume A1: a in X ; :: thesis: ( (arity-from-list B) . a <> 0 iff ex n being Nat st a in B . n )
set F = arity-from-list B;
A2: ( ( ex n being Nat st a in B . n & a in B . ((arity-from-list B) . a) ) or ( ( for n being Nat holds not a in B . n ) & (arity-from-list B) . a = 0 ) ) by A1, Def14;
thus ( (arity-from-list B) . a <> 0 implies ex n being Nat st a in B . n ) by A1, Def14; :: thesis: ( ex n being Nat st a in B . n implies (arity-from-list B) . a <> 0 )
assume ex n being Nat st a in B . n ; :: thesis: (arity-from-list B) . a <> 0
then A4: (arity-from-list B) . a in dom B by A2, Th29;
consider m being Nat such that
A5: dom B = Seg m by FINSEQ_1:def 2;
thus (arity-from-list B) . a <> 0 by FINSEQ_1:1, A4, A5; :: thesis: verum