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

assume A2:
for x being Nat holds GSq . x is acyclic
; :: thesis: GSq is acyclic assume A1:
GSq is acyclic
; :: thesis: for x being Nat holds GSq . x is acyclic

let x be Nat; :: thesis: GSq . x is acyclic

x in dom GSq by LmNat;

then x is Element of dom GSq ;

hence GSq . x is acyclic by A1; :: thesis: verum

end;let x be Nat; :: thesis: GSq . x is acyclic

x in dom GSq by LmNat;

then x is Element of dom GSq ;

hence GSq . x is acyclic by A1; :: thesis: verum

let x be Element of dom GSq; :: according to GLIB_002:def 16 :: thesis: GSq . x is acyclic

x is Nat by LmNat;

hence GSq . x is acyclic by A2; :: thesis: verum