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
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 [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) 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 [(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 :: 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) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:3, XBOOLE_1:45;
assume A35: i in the carrier of IIG ; :: thesis: M1 . b1 = M2 . b1
then reconsider v = i as Vertex of IIG ;
v in (InputVertices IIG) \/ (InnerVertices IIG) by A35, XBOOLE_1:45;
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 (InnerVertices IIG) \ (SortsWithConstants IIG) ) by A34, A36, XBOOLE_0:def 3;
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 A33, A37; :: 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 [(action_at v), the carrier of IIG]) by A32;
hence M1 . i = M2 . i by A33, A38; :: thesis: verum
end;
suppose A39: v in (InnerVertices IIG) \ (SortsWithConstants IIG) ; :: thesis: M1 . b1 = M2 . b1
then M1 . v = id (FreeGen (v, the Sorts of A)) by A32;
hence M1 . i = M2 . i by A33, A39; :: thesis: verum
end;
end;
end;
hence M1 = M2 ; :: thesis: verum