hereby :: thesis: ( ( for n being Nat holds GSq . n is acyclic ) implies 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;
assume A2: for x being Nat holds GSq . x is acyclic ; :: thesis: GSq is acyclic
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