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

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

end;

assume A2: for x being Nat holds GSq . x is connected ; :: thesis: GSq is connected
let x be Element of dom GSq; :: according to GLIB_002:def 15 :: thesis: GSq . x is connected
x is Nat by LmNat;
hence GSq . x is connected by A2; :: thesis: verum