hereby :: thesis: ( ( for n being Nat holds GSq . n is Tree-like ) implies GSq is Tree-like )

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

end;

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