let M1, M2 be ManySortedFunction of FreeGen the Sorts of A,the Sorts of (FreeEnv A); :: thesis: ( ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies M1 . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M1 . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M1 . v = id (FreeGen v,the Sorts of A) ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies M2 . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M2 . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M2 . v = id (FreeGen v,the Sorts of A) ) ) ) implies M1 = M2 )
assume that
A42: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies M1 . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M1 . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M1 . v = id (FreeGen v,the Sorts of A) ) ) and
A43: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies M2 . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M2 . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M2 . v = id (FreeGen v,the Sorts of A) ) ) ; :: thesis: M1 = M2

now

let i be set ; :: thesis: ( i in the carrier of IIG implies M1 . b₁ = M2 . b₁ )
assume A44: i in the carrier of IIG ; :: thesis: M1 . b₁ = M2 . b₁
then reconsider v = i as Vertex of IIG ;
A45: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:5, XBOOLE_1:45;
v in (InputVertices IIG) \/ (InnerVertices IIG) by A44, XBOOLE_1:45;
then A46: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def 3;

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

suppose A47: v in InputVertices IIG ; :: thesis: M1 . b₁ = M2 . b₁

then M1 . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) by A42;
hence M1 . i = M2 . i by A43, A47; :: thesis: verum

end;

suppose A48: v in SortsWithConstants IIG ; :: thesis: M1 . b₁ = M2 . b₁

then M1 . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) by A42;
hence M1 . i = M2 . i by A43, A48; :: thesis: verum

end;

suppose A49: v in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis: M1 . b₁ = M2 . b₁

then M1 . v = id (FreeGen v,the Sorts of A) by A42;
hence M1 . i = M2 . i by A43, A49; :: thesis: verum

end;

end;

end;

hence M1 = M2 by PBOOLE:3; :: thesis: verum