hereby :: thesis: ( ( for x being Nat holds GSq . x is non-Dmulti ) implies GSq is non-Dmulti )

assume A1: GSq is non-Dmulti ; :: thesis: for x being Nat holds GSq . x is non-Dmulti
let x be Nat; :: thesis: GSq . x is non-Dmulti
x in dom GSq by LmNat;
hence GSq . x is non-Dmulti by A1; :: thesis: verum

end;

assume A2: for x being Nat holds GSq . x is non-Dmulti ; :: thesis: GSq is non-Dmulti
let x be Element of dom GSq; :: according to GLIB_000:def 71 :: thesis: GSq . x is non-Dmulti
thus GSq . x is non-Dmulti by A2; :: thesis: verum