defpred S_{1}[ object , object ] means ex v being Vertex of IIG st

( v = $1 & ( $1 in InputVertices IIG implies $2 = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( $1 in SortsWithConstants IIG implies $2 = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( $1 in (InnerVertices IIG) \ (SortsWithConstants IIG) implies $2 = id (FreeGen (v, the Sorts of A)) ) );

A11: for i being object st i in the carrier of IIG holds

S_{1}[i,M . i]
from PBOOLE:sch 3(A1);

reconsider M = M as ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) by A12, PBOOLE:def 15;

take M ; :: thesis: for v being Vertex of IIG holds

( ( v in InputVertices IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M . v = id (FreeGen (v, the Sorts of A)) ) )

let v be Vertex of IIG; :: thesis: ( ( v in InputVertices IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M . v = id (FreeGen (v, the Sorts of A)) ) )

S_{1}[v,M . v]
by A11;

hence M . v = id (FreeGen (v, the Sorts of A)) by A31; :: thesis: verum

( v = $1 & ( $1 in InputVertices IIG implies $2 = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( $1 in SortsWithConstants IIG implies $2 = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( $1 in (InnerVertices IIG) \ (SortsWithConstants IIG) implies $2 = id (FreeGen (v, the Sorts of A)) ) );

A1: now :: thesis: for i being object st i in the carrier of IIG holds

ex j being object st S_{1}[i,j]

consider M being ManySortedSet of the carrier of IIG such that ex j being object st S

let i be object ; :: thesis: ( i in the carrier of IIG implies ex j being object st S_{1}[i,j] )

assume A2: i in the carrier of IIG ; :: thesis: ex j being object st S_{1}[i,j]

then reconsider v = i as Vertex of IIG ;

v in (InputVertices IIG) \/ (InnerVertices IIG) by A2, XBOOLE_1:45;

then A3: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def 3;

A4: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:3, XBOOLE_1:45;

thus ex j being object st S_{1}[i,j]
:: thesis: verum

end;assume A2: i in the carrier of IIG ; :: thesis: ex j being object st S

then reconsider v = i as Vertex of IIG ;

v in (InputVertices IIG) \/ (InnerVertices IIG) by A2, XBOOLE_1:45;

then A3: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def 3;

A4: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:3, XBOOLE_1:45;

thus ex j being object st S

proof
end;

per cases
( v in InputVertices IIG or v in SortsWithConstants IIG or v in (InnerVertices IIG) \ (SortsWithConstants IIG) )
by A4, A3, XBOOLE_0:def 3;

end;

suppose A5:
v in InputVertices IIG
; :: thesis: ex j being object st S_{1}[i,j]

reconsider j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) as set ;

take j ; :: thesis: S_{1}[i,j]

take v ; :: thesis: ( v = i & ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus v = i ; :: thesis: ( ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) ; :: thesis: ( ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) by A5, MSAFREE2:4, XBOOLE_0:3; :: thesis: ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) )

A6: ( (InnerVertices IIG) \ (SortsWithConstants IIG) c= InnerVertices IIG & InputVertices IIG misses InnerVertices IIG ) by XBOOLE_1:36, XBOOLE_1:79;

assume i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis: j = id (FreeGen (v, the Sorts of A))

hence j = id (FreeGen (v, the Sorts of A)) by A5, A6, XBOOLE_0:3; :: thesis: verum

end;take j ; :: thesis: S

take v ; :: thesis: ( v = i & ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus v = i ; :: thesis: ( ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) ; :: thesis: ( ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) by A5, MSAFREE2:4, XBOOLE_0:3; :: thesis: ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) )

A6: ( (InnerVertices IIG) \ (SortsWithConstants IIG) c= InnerVertices IIG & InputVertices IIG misses InnerVertices IIG ) by XBOOLE_1:36, XBOOLE_1:79;

assume i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis: j = id (FreeGen (v, the Sorts of A))

hence j = id (FreeGen (v, the Sorts of A)) by A5, A6, XBOOLE_0:3; :: thesis: verum

suppose A7:
v in SortsWithConstants IIG
; :: thesis: ex j being object st S_{1}[i,j]

reconsider j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) as set ;

take j ; :: thesis: S_{1}[i,j]

take v ; :: thesis: ( v = i & ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus v = i ; :: thesis: ( ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) by A7, MSAFREE2:4, XBOOLE_0:3; :: thesis: ( ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) ; :: thesis: ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) )

A8: (InnerVertices IIG) \ (SortsWithConstants IIG) misses SortsWithConstants IIG by XBOOLE_1:79;

assume i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis: j = id (FreeGen (v, the Sorts of A))

hence j = id (FreeGen (v, the Sorts of A)) by A7, A8, XBOOLE_0:3; :: thesis: verum

end;take j ; :: thesis: S

take v ; :: thesis: ( v = i & ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus v = i ; :: thesis: ( ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) by A7, MSAFREE2:4, XBOOLE_0:3; :: thesis: ( ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) ; :: thesis: ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) )

A8: (InnerVertices IIG) \ (SortsWithConstants IIG) misses SortsWithConstants IIG by XBOOLE_1:79;

assume i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis: j = id (FreeGen (v, the Sorts of A))

hence j = id (FreeGen (v, the Sorts of A)) by A7, A8, XBOOLE_0:3; :: thesis: verum

suppose A9:
v in (InnerVertices IIG) \ (SortsWithConstants IIG)
; :: thesis: ex j being object st S_{1}[i,j]

reconsider j = id (FreeGen (v, the Sorts of A)) as set ;

take j ; :: thesis: S_{1}[i,j]

take v ; :: thesis: ( v = i & ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus v = i ; :: thesis: ( ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

assume i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis: j = id (FreeGen (v, the Sorts of A))

thus j = id (FreeGen (v, the Sorts of A)) ; :: thesis: verum

end;take j ; :: thesis: S

take v ; :: thesis: ( v = i & ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus v = i ; :: thesis: ( ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

hereby :: thesis: ( ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )

thus
( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) )
by A9, XBOOLE_0:3, XBOOLE_1:79; :: thesis: ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) )A10:
( (InnerVertices IIG) \ (SortsWithConstants IIG) c= InnerVertices IIG & InputVertices IIG misses InnerVertices IIG )
by XBOOLE_1:36, XBOOLE_1:79;

assume i in InputVertices IIG ; :: thesis: j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v])

hence j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A9, A10, XBOOLE_0:3; :: thesis: verum

end;assume i in InputVertices IIG ; :: thesis: j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v])

hence j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A9, A10, XBOOLE_0:3; :: thesis: verum

assume i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis: j = id (FreeGen (v, the Sorts of A))

thus j = id (FreeGen (v, the Sorts of A)) ; :: thesis: verum

A11: for i being object st i in the carrier of IIG holds

S

A12: now :: thesis: for i being object st i in the carrier of IIG holds

M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i)

M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i)

let i be object ; :: thesis: ( i in the carrier of IIG implies M . b_{1} is Function of ((FreeGen the Sorts of A) . b_{1}),( the Sorts of (FreeEnv A) . b_{1}) )

A13: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:3, XBOOLE_1:45;

assume A14: i in the carrier of IIG ; :: thesis: M . b_{1} is Function of ((FreeGen the Sorts of A) . b_{1}),( the Sorts of (FreeEnv A) . b_{1})

then reconsider v = i as Vertex of IIG ;

v in (InputVertices IIG) \/ (InnerVertices IIG) by A14, XBOOLE_1:45;

then A15: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def 3;

A16: FreeGen (v, the Sorts of A) = (FreeGen the Sorts of A) . v by MSAFREE:def 16;

A17: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 14;

end;A13: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:3, XBOOLE_1:45;

assume A14: i in the carrier of IIG ; :: thesis: M . b

then reconsider v = i as Vertex of IIG ;

v in (InputVertices IIG) \/ (InnerVertices IIG) by A14, XBOOLE_1:45;

then A15: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def 3;

A16: FreeGen (v, the Sorts of A) = (FreeGen the Sorts of A) . v by MSAFREE:def 16;

A17: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 14;

per cases
( v in InputVertices IIG or v in SortsWithConstants IIG or v in (InnerVertices IIG) \ (SortsWithConstants IIG) )
by A13, A15, XBOOLE_0:def 3;

end;

suppose A18:
v in InputVertices IIG
; :: thesis: M . b_{1} is Function of ((FreeGen the Sorts of A) . b_{1}),( the Sorts of (FreeEnv A) . b_{1})

then
iv . v in the Sorts of A . v
by MSAFREE2:def 5;

then A19: root-tree [(iv . v),v] in FreeGen (v, the Sorts of A) by MSAFREE:def 15;

S_{1}[v,M . v]
by A11;

hence M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A16, A17, A18, A19, FUNCOP_1:45; :: thesis: verum

end;then A19: root-tree [(iv . v),v] in FreeGen (v, the Sorts of A) by MSAFREE:def 15;

S

hence M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A16, A17, A18, A19, FUNCOP_1:45; :: thesis: verum

suppose A20:
v in SortsWithConstants IIG
; :: thesis: M . b_{1} is Function of ((FreeGen the Sorts of A) . b_{1}),( the Sorts of (FreeEnv A) . b_{1})

reconsider sy = Sym ((action_at v), the Sorts of A) as NonTerminal of (DTConMSA the Sorts of A) ;

set p = <*> (TS (DTConMSA the Sorts of A));

set e = root-tree [(action_at v), the carrier of IIG];

A21: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;

v in { s where s is SortSymbol of IIG : s is with_const_op } by A20, MSAFREE2:def 1;

then ex s being SortSymbol of IIG st

( v = s & s is with_const_op ) ;

then consider o being OperSymbol of IIG such that

A22: the Arity of IIG . o = {} and

A23: the ResultSort of IIG . o = v by MSUALG_2:def 1;

A24: for n being Nat st n in dom (<*> (TS (DTConMSA the Sorts of A))) holds

(<*> (TS (DTConMSA the Sorts of A))) . n in FreeSort ( the Sorts of A,((the_arity_of o) /. n)) ;

<*> (TS (DTConMSA the Sorts of A)) = the_arity_of o by A22, MSUALG_1:def 1;

then A25: <*> (TS (DTConMSA the Sorts of A)) in (((FreeSort the Sorts of A) #) * the Arity of IIG) . o by A24, MSAFREE:9;

the_result_sort_of o = v by A23, MSUALG_1:def 2;

then o = action_at v by A20, A21, MSAFREE2:def 7;

then sy ==> roots (<*> (TS (DTConMSA the Sorts of A))) by A25, MSAFREE:10;

then ( {} = <*> (IIG -Terms the Sorts of A) & <*> (TS (DTConMSA the Sorts of A)) is SubtreeSeq of Sym ((action_at v), the Sorts of A) ) by DTCONSTR:def 6;

then ( root-tree [(action_at v), the carrier of IIG] = [(action_at v), the carrier of IIG] -tree {} & {} is ArgumentSeq of sy ) by MSATERM:def 2, TREES_4:20;

then root-tree [(action_at v), the carrier of IIG] in IIG -Terms the Sorts of A by MSATERM:1;

then reconsider e = root-tree [(action_at v), the carrier of IIG] as Element of TS (DTConMSA the Sorts of A) by MSATERM:def 1;

( e . {} = [(action_at v), the carrier of IIG] & the_result_sort_of (action_at v) = v ) by A20, A21, MSAFREE2:def 7, TREES_4:3;

then e in { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st

( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st

( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) } ;

then e in FreeSort ( the Sorts of A,v) by MSAFREE:def 10;

then A26: e in the Sorts of (FreeEnv A) . v by A17, MSAFREE:def 11;

S_{1}[v,M . v]
by A11;

hence M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A16, A20, A26, FUNCOP_1:45; :: thesis: verum

end;set p = <*> (TS (DTConMSA the Sorts of A));

set e = root-tree [(action_at v), the carrier of IIG];

A21: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;

v in { s where s is SortSymbol of IIG : s is with_const_op } by A20, MSAFREE2:def 1;

then ex s being SortSymbol of IIG st

( v = s & s is with_const_op ) ;

then consider o being OperSymbol of IIG such that

A22: the Arity of IIG . o = {} and

A23: the ResultSort of IIG . o = v by MSUALG_2:def 1;

A24: for n being Nat st n in dom (<*> (TS (DTConMSA the Sorts of A))) holds

(<*> (TS (DTConMSA the Sorts of A))) . n in FreeSort ( the Sorts of A,((the_arity_of o) /. n)) ;

<*> (TS (DTConMSA the Sorts of A)) = the_arity_of o by A22, MSUALG_1:def 1;

then A25: <*> (TS (DTConMSA the Sorts of A)) in (((FreeSort the Sorts of A) #) * the Arity of IIG) . o by A24, MSAFREE:9;

the_result_sort_of o = v by A23, MSUALG_1:def 2;

then o = action_at v by A20, A21, MSAFREE2:def 7;

then sy ==> roots (<*> (TS (DTConMSA the Sorts of A))) by A25, MSAFREE:10;

then ( {} = <*> (IIG -Terms the Sorts of A) & <*> (TS (DTConMSA the Sorts of A)) is SubtreeSeq of Sym ((action_at v), the Sorts of A) ) by DTCONSTR:def 6;

then ( root-tree [(action_at v), the carrier of IIG] = [(action_at v), the carrier of IIG] -tree {} & {} is ArgumentSeq of sy ) by MSATERM:def 2, TREES_4:20;

then root-tree [(action_at v), the carrier of IIG] in IIG -Terms the Sorts of A by MSATERM:1;

then reconsider e = root-tree [(action_at v), the carrier of IIG] as Element of TS (DTConMSA the Sorts of A) by MSATERM:def 1;

( e . {} = [(action_at v), the carrier of IIG] & the_result_sort_of (action_at v) = v ) by A20, A21, MSAFREE2:def 7, TREES_4:3;

then e in { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st

( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st

( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) } ;

then e in FreeSort ( the Sorts of A,v) by MSAFREE:def 10;

then A26: e in the Sorts of (FreeEnv A) . v by A17, MSAFREE:def 11;

S

hence M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A16, A20, A26, FUNCOP_1:45; :: thesis: verum

suppose A27:
v in (InnerVertices IIG) \ (SortsWithConstants IIG)
; :: thesis: M . b_{1} is Function of ((FreeGen the Sorts of A) . b_{1}),( the Sorts of (FreeEnv A) . b_{1})

A28:
( dom (id (FreeGen (v, the Sorts of A))) = FreeGen (v, the Sorts of A) & rng (id (FreeGen (v, the Sorts of A))) = FreeGen (v, the Sorts of A) )
;

S_{1}[v,M . v]
by A11;

hence M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A16, A17, A27, A28, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;S

hence M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A16, A17, A27, A28, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

now :: thesis: for i being object st i in dom M holds

M . i is Function

then reconsider M = M as ManySortedFunction of the carrier of IIG by FUNCOP_1:def 6;M . i is Function

let i be object ; :: thesis: ( i in dom M implies M . i is Function )

assume i in dom M ; :: thesis: M . i is Function

then i in the carrier of IIG by PARTFUN1:def 2;

hence M . i is Function by A12; :: thesis: verum

end;assume i in dom M ; :: thesis: M . i is Function

then i in the carrier of IIG by PARTFUN1:def 2;

hence M . i is Function by A12; :: thesis: verum

reconsider M = M as ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) by A12, PBOOLE:def 15;

take M ; :: thesis: for v being Vertex of IIG holds

( ( v in InputVertices IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M . v = id (FreeGen (v, the Sorts of A)) ) )

let v be Vertex of IIG; :: thesis: ( ( v in InputVertices IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M . v = id (FreeGen (v, the Sorts of A)) ) )

hereby :: thesis: ( ( v in SortsWithConstants IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M . v = id (FreeGen (v, the Sorts of A)) ) )

assume A29:
v in InputVertices IIG
; :: thesis: M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v])

S_{1}[v,M . v]
by A11;

hence M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A29; :: thesis: verum

end;S

hence M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A29; :: thesis: verum

hereby :: thesis: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M . v = id (FreeGen (v, the Sorts of A)) )

assume A31:
v in (InnerVertices IIG) \ (SortsWithConstants IIG)
; :: thesis: M . v = id (FreeGen (v, the Sorts of A))assume A30:
v in SortsWithConstants IIG
; :: thesis: M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG])

S_{1}[v,M . v]
by A11;

hence M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) by A30; :: thesis: verum

end;S

hence M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) by A30; :: thesis: verum

S

hence M . v = id (FreeGen (v, the Sorts of A)) by A31; :: thesis: verum