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 implies f in St (x '=' y),E ) & ( f in St (x '=' y),E implies E,f |= x '=' y ) & ( f in St (x '=' y),E implies f . x = f . y ) & ( f . x = f . y implies f in St (x '=' y),E ) ) by Def4, Th2;
hence ( E,f |= x '=' y iff f . x = f . y ) ; :: thesis: verum