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 ;
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 set st S₁[i,j] :: thesis:

proof

per cases by A4, A3, 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:

A6: InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:4;
assume i in SortsWithConstants IIG ; :: thesis:
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;

A7: ( (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:
hence j = id (FreeGen (v, the Sorts of A)) by A5, A7, XBOOLE_0:3; :: thesis:

end;

suppose A8: 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:

A9: InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:4;
assume i in InputVertices IIG ; :: thesis:
hence j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A8, A9, 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:
A10: (InnerVertices IIG) \ (SortsWithConstants IIG) misses SortsWithConstants IIG by XBOOLE_1:79;
assume i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis:
hence j = id (FreeGen (v, the Sorts of A)) by A8, A10, XBOOLE_0:3; :: thesis:

end;

suppose A11: 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:

A12: ( (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:
hence j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A11, A12, XBOOLE_0:3; :: thesis:

end;

hereby :: thesis:

A13: (InnerVertices IIG) \ (SortsWithConstants IIG) misses SortsWithConstants IIG by XBOOLE_1:79;
assume i in SortsWithConstants IIG ; :: thesis:
hence j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) by A11, A13, 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 the carrier of IIG such that
A14: for i being set st i in the carrier of IIG holds
S₁[i,M . i] from PBOOLE:sch 3(A1);

A15: now

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

per cases by A16, A18, XBOOLE_0:def 3;

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

then iv . v in the Sorts of A . v by MSAFREE2:def 5;
then A22: root-tree [(iv . v),v] in FreeGen (v, the Sorts of A) by MSAFREE:def 15;
S₁[v,M . v] by A14;
hence M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A19, A20, A21, A22, FUNCOP_1:45; :: thesis:

end;

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

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];
A24: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;
v in { s where s is SortSymbol of IIG : s is with_const_op } by A23, 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
A25: the Arity of IIG . o = {} and
A26: the ResultSort of IIG . o = v by MSUALG_2:def 1;
A27: 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 A25, MSUALG_1:def 1;
then A28: <*> (TS (DTConMSA the Sorts of A)) in (((FreeSort the Sorts of A) #) * the Arity of IIG) . o by A27, MSAFREE:9;
the_result_sort_of o = v by A26, MSUALG_1:def 2;
then o = action_at v by A23, A24, MSAFREE2:def 7;
then sy ==> roots (<*> (TS (DTConMSA the Sorts of A))) by A28, 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 A23, A24, 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 A29: e in the Sorts of (FreeEnv A) . v by A20, MSAFREE:def 11;
S₁[v,M . v] by A14;
hence M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A19, A23, A29, FUNCOP_1:45; :: thesis:

end;

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

A31: ( 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:45;
S₁[v,M . v] by A14;
hence M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A19, A20, A30, A31, FUNCT_2:def 1, RELSET_1:4; :: thesis:

end;

now

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

end;

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

hereby :: thesis:

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

end;

hereby :: thesis:

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

end;

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