defpred S₁[ set , set ] 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) ) );

A1: now

let i be set ; :: thesis:
assume A2: i in the carrier of IIG ; :: thesis:
then reconsider v = i as Vertex of IIG ;
A3: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:5, XBOOLE_1:45;
v in (InputVertices IIG) \/ (InnerVertices IIG) by A2, XBOOLE_1:45;
then A4: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def 3;
thus ex j being set st S₁[i,j] :: thesis:

proof

per cases by A3, A4, XBOOLE_0:def 3;

suppose A5: v in InputVertices IIG ; :: thesis:

reconsider j = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) as set ;
take j ; :: thesis:
take v ; :: thesis:
thus v = i ; :: thesis:
thus ( i in InputVertices IIG implies j = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) ) ; :: thesis:

hereby :: thesis:

assume A6: i in SortsWithConstants IIG ; :: thesis:
InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:6;
hence j = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) by A5, A6, XBOOLE_0:3; :: thesis:

end;

assume A7: i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis:
A8: (InnerVertices IIG) \ (SortsWithConstants IIG) c= InnerVertices IIG by XBOOLE_1:36;
InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;
hence j = id (FreeGen v,the Sorts of A) by A5, A7, A8, XBOOLE_0:3; :: thesis:

end;

suppose A9: v in SortsWithConstants IIG ; :: thesis:

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

hereby :: thesis:

assume A10: i in InputVertices IIG ; :: thesis:
InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:6;
hence j = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) by A9, A10, XBOOLE_0:3; :: thesis:

end;

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

end;

suppose A12: v in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis:

reconsider j = id (FreeGen v,the Sorts of A) as set ;
take j ; :: thesis:
take v ; :: thesis:
thus v = i ; :: thesis:

hereby :: thesis:

assume A13: i in InputVertices IIG ; :: thesis:
A14: (InnerVertices IIG) \ (SortsWithConstants IIG) c= InnerVertices IIG by XBOOLE_1:36;
InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;
hence j = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) by A12, A13, A14, XBOOLE_0:3; :: thesis:

end;

hereby :: thesis:

assume A15: i in SortsWithConstants IIG ; :: thesis:
(InnerVertices IIG) \ (SortsWithConstants IIG) misses SortsWithConstants IIG by XBOOLE_1:79;
hence j = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) by A12, A15, XBOOLE_0:3; :: thesis:

end;

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

end;

consider M being ManySortedSet of such that
A16: for i being set st i in the carrier of IIG holds
S₁[i,M . i] from PBOOLE:sch 3(A1);

A17: now

let i be set ; :: thesis:
assume A18: i in the carrier of IIG ; :: thesis:
then reconsider v = i as Vertex of IIG ;
A19: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:5, XBOOLE_1:45;
v in (InputVertices IIG) \/ (InnerVertices IIG) by A18, XBOOLE_1:45;
then A20: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def 3;
A21: FreeGen v,the Sorts of A = (FreeGen the Sorts of A) . v by MSAFREE:def 18;
A22: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 16;

per cases by A19, A20, XBOOLE_0:def 3;

suppose A23: v in InputVertices IIG ; :: thesis:

then iv . v in the Sorts of A . v by MSAFREE2:def 5;
then A24: root-tree [(iv . v),v] in FreeGen v,the Sorts of A by MSAFREE:def 17;
S₁[v,M . v] by A16;
hence M . i is Function of ((FreeGen the Sorts of A) . i),(the Sorts of (FreeEnv A) . i) by A21, A22, A23, A24, FUNCOP_1:57; :: thesis:

end;

suppose A25: v in SortsWithConstants IIG ; :: thesis:

then v in { s where s is SortSymbol of IIG : s is with_const_op } by MSAFREE2:def 1;
then consider s being SortSymbol of IIG such that
A26: v = s and
A27: s is with_const_op ;
consider o being OperSymbol of IIG such that
A28: the Arity of IIG . o = {} and
A29: the ResultSort of IIG . o = v by A26, A27, MSUALG_2:def 2;
set e = root-tree [(action_at v),the carrier of IIG];
A30: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:5;
the_result_sort_of o = v by A29, MSUALG_1:def 7;
then A31: o = action_at v by A25, A30, MSAFREE2:def 7;
A32: root-tree [(action_at v),the carrier of IIG] = [(action_at v),the carrier of IIG] -tree {} by TREES_4:20;
A33: {} = <*> (IIG -Terms the Sorts of A) ;
set p = <*> (TS (DTConMSA the Sorts of A));
reconsider sy = Sym (action_at v),the Sorts of A as NonTerminal of (DTConMSA the Sorts of A) ;
A34: <*> (TS (DTConMSA the Sorts of A)) = the_arity_of o by A28, MSUALG_1:def 6;
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) ;
then <*> (TS (DTConMSA the Sorts of A)) in (((FreeSort the Sorts of A) # ) * the Arity of IIG) . o by A34, MSAFREE:9;
then sy ==> roots (<*> (TS (DTConMSA the Sorts of A))) by A31, MSAFREE:10;
then <*> (TS (DTConMSA the Sorts of A)) is SubtreeSeq of Sym (action_at v),the Sorts of A by DTCONSTR:def 9;
then {} is ArgumentSeq of sy by A33, MSATERM:def 2;
then root-tree [(action_at v),the carrier of IIG] in IIG -Terms the Sorts of A by A32, 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;
A35: e . {} = [(action_at v),the carrier of IIG] by TREES_4:3;
the_result_sort_of (action_at v) = v by A25, A30, MSAFREE2:def 7;
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 ) ) } by A35;
then e in FreeSort the Sorts of A,v by MSAFREE:def 12;
then A36: e in the Sorts of (FreeEnv A) . v by A22, MSAFREE:def 13;
S₁[v,M . v] by A16;
hence M . i is Function of ((FreeGen the Sorts of A) . i),(the Sorts of (FreeEnv A) . i) by A21, A25, A36, FUNCOP_1:57; :: thesis:

end;

suppose A37: v in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis:

A38: ( 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 ) by RELAT_1:71;
S₁[v,M . v] by A16;
hence M . i is Function of ((FreeGen the Sorts of A) . i),(the Sorts of (FreeEnv A) . i) by A21, A22, A37, A38, FUNCT_2:def 1, RELSET_1:11; :: thesis:

end;

now

let i be set ; :: thesis:
assume i in dom M ; :: thesis:
then i in the carrier of IIG by PARTFUN1:def 4;
hence M . i is Function by A17; :: thesis:

end;

then reconsider M = M as ManySortedFunction of by FUNCOP_1:def 6;
reconsider M = M as ManySortedFunction of FreeGen the Sorts of A,the Sorts of (FreeEnv A) by A17, PBOOLE:def 18;
take M ; :: thesis:
let v be Vertex of IIG; :: thesis:

hereby :: thesis:

assume A39: v in InputVertices IIG ; :: thesis:
S₁[v,M . v] by A16;
hence M . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) by A39; :: thesis:

end;

hereby :: thesis:

assume A40: v in SortsWithConstants IIG ; :: thesis:
S₁[v,M . v] by A16;
hence M . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) by A40; :: thesis:

end;

assume A41: v in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis:
S₁[v,M . v] by A16;
hence M . v = id (FreeGen v,the Sorts of A) by A41; :: thesis: