hereby :: thesis: ( ( for n being Nat holds GSq . n is loopfull ) implies GSq is loopfull )

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

end;

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