let S be non empty non void ManySortedSign ; :: thesis: for U0, U1 being non-empty MSAlgebra of S
for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds
U1 |= E
let U0, U1 be non-empty MSAlgebra of S; :: thesis: for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds
U1 |= E
let E be EqualSet of S; :: thesis: ( U0,U1 are_isomorphic & U0 |= E implies U1 |= E )
assume that
A1: U0,U1 are_isomorphic and
A2: U0 |= E ; :: thesis: U1 |= E
let s be SortSymbol of S; :: according to EQUATION:def 6 :: thesis: for e being Element of (Equations S) . s st e in E . s holds
U1 |= e
let e be Element of (Equations S) . s; :: thesis: ( e in E . s implies U1 |= e )
assume e in E . s ; :: thesis: U1 |= e
then U0 |= e by A2, Def6;
hence U1 |= e by A1, Th35; :: thesis: verum