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