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
A35: 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
A36: 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₁ )
A37: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:5, XBOOLE_1:45;
assume A38: i in the carrier of IIG ; :: thesis: M1 . b₁ = M2 . b₁
then reconsider v = i as Vertex of IIG ;
v in (InputVertices IIG) \/ (InnerVertices IIG) by A38, XBOOLE_1:45;
then A39: ( 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 A37, A39, XBOOLE_0:def 3;

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

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

end;

suppose A41: 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 A35;
hence M1 . i = M2 . i by A36, A41; :: thesis: verum

end;

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

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

end;

end;

end;

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