let E be non empty set ; :: thesis: for f being Function of VAR,E
for x, y being Variable holds
( E,f |= x '=' y iff f . x = f . y )
let f be Function of VAR,E; :: thesis: for x, y being Variable holds
( E,f |= x '=' y iff f . x = f . y )
let x, y be Variable; :: thesis: ( E,f |= x '=' y iff f . x = f . y )
( E,f |= x '=' y iff f in St ((x '=' y),E) ) by Def4;
hence ( E,f |= x '=' y iff f . x = f . y ) by Th2; :: thesis: verum