set O = OwnSymbolsOf S;

set SS = AllSymbolsOf S;

let IT1, IT2 be Function; :: thesis: ( dom IT1 = OwnSymbolsOf S & ( for s being own Element of S holds IT1 . s = X -freeInterpreter s ) & dom IT2 = OwnSymbolsOf S & ( for s being own Element of S holds IT2 . s = X -freeInterpreter s ) implies IT1 = IT2 )

assume A5: ( dom IT1 = OwnSymbolsOf S & ( for s being own Element of S holds IT1 . s = X -freeInterpreter s ) ) ; :: thesis: ( not dom IT2 = OwnSymbolsOf S or ex s being own Element of S st not IT2 . s = X -freeInterpreter s or IT1 = IT2 )

assume A6: ( dom IT2 = OwnSymbolsOf S & ( for s being own Element of S holds IT2 . s = X -freeInterpreter s ) ) ; :: thesis: IT1 = IT2

set SS = AllSymbolsOf S;

let IT1, IT2 be Function; :: thesis: ( dom IT1 = OwnSymbolsOf S & ( for s being own Element of S holds IT1 . s = X -freeInterpreter s ) & dom IT2 = OwnSymbolsOf S & ( for s being own Element of S holds IT2 . s = X -freeInterpreter s ) implies IT1 = IT2 )

assume A5: ( dom IT1 = OwnSymbolsOf S & ( for s being own Element of S holds IT1 . s = X -freeInterpreter s ) ) ; :: thesis: ( not dom IT2 = OwnSymbolsOf S or ex s being own Element of S st not IT2 . s = X -freeInterpreter s or IT1 = IT2 )

assume A6: ( dom IT2 = OwnSymbolsOf S & ( for s being own Element of S holds IT2 . s = X -freeInterpreter s ) ) ; :: thesis: IT1 = IT2

now :: thesis: ( dom IT1 = dom IT2 & ( for x being object st x in dom IT1 holds

IT1 . x = IT2 . x ) )

hence
IT1 = IT2
by FUNCT_1:2; :: thesis: verumIT1 . x = IT2 . x ) )

thus
dom IT1 = dom IT2
by A5, A6; :: thesis: for x being object st x in dom IT1 holds

IT1 . x = IT2 . x

let x be object ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )

assume x in dom IT1 ; :: thesis: IT1 . x = IT2 . x

then reconsider s = x as own Element of S by FOMODEL1:def 19, A5;

IT1 . s = X -freeInterpreter s by A5

.= IT2 . s by A6 ;

hence IT1 . x = IT2 . x ; :: thesis: verum

end;IT1 . x = IT2 . x

let x be object ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )

assume x in dom IT1 ; :: thesis: IT1 . x = IT2 . x

then reconsider s = x as own Element of S by FOMODEL1:def 19, A5;

IT1 . s = X -freeInterpreter s by A5

.= IT2 . s by A6 ;

hence IT1 . x = IT2 . x ; :: thesis: verum