let T1, T2 be MSSubset of (FreeMSA Y); :: thesis: ( ( for s being SortSymbol of S holds T1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) & ( for s being SortSymbol of S holds T2 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) implies T1 = T2 )

assume that

A3: for s being SortSymbol of S holds T1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } and

A4: for s being SortSymbol of S holds T2 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ; :: thesis: T1 = T2

assume that

A3: for s being SortSymbol of S holds T1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } and

A4: for s being SortSymbol of S holds T2 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ; :: thesis: T1 = T2

now :: thesis: for s being object st s in the carrier of S holds

T1 . s = T2 . s

hence
T1 = T2
; :: thesis: verumT1 . s = T2 . s

let s be object ; :: thesis: ( s in the carrier of S implies T1 . s = T2 . s )

assume A5: s in the carrier of S ; :: thesis: T1 . s = T2 . s

hence T1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } by A3

.= T2 . s by A4, A5 ;

:: thesis: verum

end;assume A5: s in the carrier of S ; :: thesis: T1 . s = T2 . s

hence T1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } by A3

.= T2 . s by A4, A5 ;

:: thesis: verum