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

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

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