let M1, M2 be ManySortedFunction of FreeGen the Sorts of A, the Sorts of (); :: 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 [(), the carrier of IIG]) ) & ( v in () \ () 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 [(), the carrier of IIG]) ) & ( v in () \ () implies M2 . v = id (FreeGen (v, the Sorts of A)) ) ) ) implies M1 = M2 )

assume that
A32: 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 [(), the carrier of IIG]) ) & ( v in () \ () implies M1 . v = id (FreeGen (v, the Sorts of A)) ) ) and
A33: 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 [(), the carrier of IIG]) ) & ( v in () \ () implies M2 . v = id (FreeGen (v, the Sorts of A)) ) ) ; :: thesis: M1 = M2
now :: thesis: for i being object st i in the carrier of IIG holds
M1 . i = M2 . i
let i be object ; :: thesis: ( i in the carrier of IIG implies M1 . b1 = M2 . b1 )
A34: ((InnerVertices IIG) \ ()) \/ () = InnerVertices IIG by ;
assume A35: i in the carrier of IIG ; :: thesis: M1 . b1 = M2 . b1
then reconsider v = i as Vertex of IIG ;
v in () \/ () by ;
then A36: ( 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 () \ () ) by ;
suppose A37: v in InputVertices IIG ; :: thesis: M1 . b1 = M2 . b1
then M1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A32;
hence M1 . i = M2 . i by ; :: thesis: verum
end;
suppose A38: v in SortsWithConstants IIG ; :: thesis: M1 . b1 = M2 . b1
then M1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(), the carrier of IIG]) by A32;
hence M1 . i = M2 . i by ; :: thesis: verum
end;
suppose A39: v in () \ () ; :: thesis: M1 . b1 = M2 . b1
then M1 . v = id (FreeGen (v, the Sorts of A)) by A32;
hence M1 . i = M2 . i by ; :: thesis: verum
end;
end;
end;
hence M1 = M2 ; :: thesis: verum