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

assume A2:
for x being Nat holds GSq . x is connected
; :: thesis: 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;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

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