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

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

end;

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