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

now :: thesis: for s being object st s in the carrier of S holds
T1 . 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;

hence T1 = T2 ; :: thesis: verum