let V1, V2 be ManySortedSet of the carrier of C; :: thesis: ( V1 . a_Type = {} & V1 . an_Adj = {} & V1 . a_Term = Vars & V2 . a_Type = {} & V2 . an_Adj = {} & V2 . a_Term = Vars implies V1 = V2 )
assume that
A2: V1 . a_Type = {} and
A3: V1 . an_Adj = {} and
A4: V1 . a_Term = Vars and
A5: V2 . a_Type = {} and
A6: V2 . an_Adj = {} and
A7: V2 . a_Term = Vars ; :: thesis: V1 = V2
now :: thesis: for x being object st x in the carrier of C holds
V1 . x = V2 . x
let x be object ; :: thesis: ( x in the carrier of C implies V1 . x = V2 . x )
assume x in the carrier of C ; :: thesis: V1 . x = V2 . x
then ( x = a_Type or x = an_Adj or x = a_Term ) by A1, ENUMSET1:def 1;
hence V1 . x = V2 . x by A2, A3, A4, A5, A6, A7; :: thesis: verum
end;
hence V1 = V2 ; :: thesis: verum