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

assume A1: GSq is plain ; :: thesis: for x being Nat holds GSq . x is plain
let x be Nat; :: thesis: GSq . x is plain
x in dom GSq by Lm4;
hence GSq . x is plain by A1; :: thesis: verum

end;

assume A2: for x being Nat holds GSq . x is plain ; :: thesis: GSq is plain
let x be Element of dom GSq; :: according to GLIBPRE0:def 2 :: thesis: GSq . x is plain
thus GSq . x is plain by A2; :: thesis: verum