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

A1: now :: thesis:

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

end;

suppose A7: 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:
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:
thus ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) ; :: thesis:
A8: (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 A7, A8, XBOOLE_0:3; :: thesis:

end;

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

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:
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]) ) by A9, XBOOLE_0:3, XBOOLE_1:79; :: thesis:
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
A11: for i being object st i in the carrier of IIG holds
S₁[i,M . i] from PBOOLE:sch 3(A1);

A12: now :: thesis:

let i be object ; :: thesis:
A13: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:3, XBOOLE_1:45;
assume A14: i in the carrier of IIG ; :: thesis:
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 by A13, A15, XBOOLE_0:def 3;

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

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₁[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:

end;

suppose A20: 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];
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₁[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:

end;

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

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₁[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:

end;

now :: thesis:

let i be object ; :: thesis:
assume i in dom M ; :: thesis:
then i in the carrier of IIG by PARTFUN1:def 2;
hence M . i is Function by A12; :: 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 A12, PBOOLE:def 15;
take M ; :: thesis:
let v be Vertex of IIG; :: thesis:

hereby :: thesis:

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

end;

hereby :: thesis:

assume A30: v in SortsWithConstants IIG ; :: thesis:
S₁[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:

end;

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