let S1, S2 be non empty 1-sorted ; :: thesis: ( the carrier of S1 = the carrier of S2 implies for N being constant net of S1 holds N is constant net of S2 )
assume A1: the carrier of S1 = the carrier of S2 ; :: thesis: for N being constant net of S1 holds N is constant net of S2
let N be constant net of S1; :: thesis: N is constant net of S2
reconsider M = N as net of S2 by A1;
the mapping of N is constant ;
then the mapping of M is constant ;
hence N is constant net of S2 by Def4; :: thesis: verum