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

( ( 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

hence
M1 = M2
; :: thesis: verumM1 . i = M2 . i

let i be object ; :: thesis: ( i in the carrier of IIG implies M1 . b_{1} = M2 . b_{1} )

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 . b_{1} = M2 . b_{1}

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;

end;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 . b

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;

end;

suppose A37:
v in InputVertices IIG
; :: thesis: M1 . b_{1} = M2 . b_{1}

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;hence M1 . i = M2 . i by A33, A37; :: thesis: verum