let X be set ; :: thesis: for B being disjoint_valued FinSequence of bool X
for a being object
for n being Nat st a in B . n holds
(arity-from-list B) . a = n
let B be disjoint_valued FinSequence of bool X; :: thesis: for a being object
for n being Nat st a in B . n holds
(arity-from-list B) . a = n
let a be object ; :: thesis: for n being Nat st a in B . n holds
(arity-from-list B) . a = n
let n be Nat; :: thesis: ( a in B . n implies (arity-from-list B) . a = n )
set F = arity-from-list B;
assume A2: a in B . n ; :: thesis: (arity-from-list B) . a = n
then n in dom B by Th29;
then A4: B . n in rng B by FUNCT_1:def 3;
rng B c= bool X by FINSEQ_1:def 4;
then a in B . ((arity-from-list B) . a) by A2, A4, Def14;
hence (arity-from-list B) . a = n by A2, Th29; :: thesis: verum