let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty finite-yielding MSAlgebra of IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v),the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let SCS be non-empty finite-yielding MSAlgebra of IIG; :: thesis: for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v),the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let v, w be Vertex of IIG; :: thesis: for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v),the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let e1 be Element of the Sorts of (FreeEnv SCS) . v; :: thesis: for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v),the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let q1 be DTree-yielding FinSequence; :: thesis: ( v in InnerVertices IIG & e1 = [(action_at v),the carrier of IIG] -tree q1 implies for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k )
assume that
A1: v in InnerVertices IIG and
A2: e1 = [(action_at v),the carrier of IIG] -tree q1 ; :: thesis: for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
thus for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k :: thesis: verum

proof

let k be Element of NAT ; :: thesis: ( k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w implies w = (the_arity_of (action_at v)) /. k )
assume that
A3: k in dom q1 and
A4: q1 . k in the Sorts of (FreeEnv SCS) . w ; :: thesis: w = (the_arity_of (action_at v)) /. k
reconsider av = action_at v as OperSymbol of IIG ;
e1 in the Sorts of (FreeEnv SCS) . v ;
then A5: e1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of av) by A1, MSAFREE2:def 7;
then len q1 = len (the_arity_of av) by A2, MSAFREE2:13;
then A6: k in dom (the_arity_of av) by A3, FINSEQ_3:31;
then A7: q1 . k in the Sorts of (FreeEnv SCS) . ((the_arity_of av) . k) by A2, A5, MSAFREE2:14;
A8: FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def 16;
then A9: q1 . k in (FreeSort the Sorts of SCS) . ((the_arity_of av) /. k) by A6, A7, PARTFUN1:def 8;

now

assume (the_arity_of av) /. k <> w ; :: thesis: contradiction
then (FreeSort the Sorts of SCS) . ((the_arity_of av) /. k) misses (FreeSort the Sorts of SCS) . w by MSAFREE:13;
then ((FreeSort the Sorts of SCS) . ((the_arity_of av) /. k)) /\ ((FreeSort the Sorts of SCS) . w) = {} by XBOOLE_0:def 7;
hence contradiction by A4, A8, A9, XBOOLE_0:def 4; :: thesis: verum

end;

hence w = (the_arity_of (action_at v)) /. k ; :: thesis: verum

end;