hereby :: thesis: ( ( for x being Nat holds GSq . x is Dsimple ) implies GSq is Dsimple )

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

end;

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