Copyright (c) 1990 Association of Mizar Users
environ
vocabulary VECTSP_1, FINSEQ_1, RELAT_1, FUNCT_1, O_RING_1;
notation XREAL_0, NAT_1, FUNCT_1, FINSEQ_1, STRUCT_0, RLVECT_1, VECTSP_1,
O_RING_1;
constructors NAT_1, O_RING_1, XREAL_0, XBOOLE_0;
clusters VECTSP_1, STRUCT_0, RELSET_1, NAT_1, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, REAL, SUBSET, ARITHM;
definitions O_RING_1;
theorems REAL_1, NAT_1, FINSEQ_1, O_RING_1, AXIOMS, FINSEQ_3;
begin
reserve i,j,k,l,m,n for Nat;
Lm1:
n<1 implies n=0
proof
assume n<1;
then n<0+1;
then 0<=n & n<=0 by NAT_1:18,38;
hence thesis by AXIOMS:21;
end;
Lm2:
n<>0 implies 1<=n
proof
assume n<>0;
then 0<n by NAT_1:19;
then 0+1<=n by NAT_1:38;
hence thesis;
end;
Lm3:
n<=1 implies n=0 or n=1
proof
assume n<=1;
then n<1 or n=1 by REAL_1:def 5;
hence thesis by Lm1;
end;
reserve R for non empty doubleLoopStr;
reserve x,y for Scalar of R;
reserve f,g,h for FinSequence of the carrier of R;
Lm4:
h=f^g iff ( dom h = Seg(len f + len g) &
(for k st k in dom f holds h.:k=f.:k) &
(for k st k in dom g holds h.:(len f + k)=g.:k))
proof
thus h=f^g implies
(dom h = Seg(len f + len g) &
(for k st k in dom f holds h.:k=f.:k) &
(for k st k in dom g holds h.:(len f + k)=g.:k))
proof
assume A1:h=f^g;
hence dom h = Seg(len f + len g) by FINSEQ_1:def 7;
then A2:len h=len f+len g by FINSEQ_1:def 3;
thus for k st k in dom f holds h.:k=f.:k
proof
let k such that A3:k in dom f;
A4:len f<=len f+len g by NAT_1:29;
A5:0<>k & k<=len f by A3,FINSEQ_3:27;
then 0<>k & k<=len h by A2,A4,AXIOMS:22;
then h.:k=h.k by O_RING_1:def 1
.=f.k by A1,A3,FINSEQ_1:def 7
.=f.:k by A5,O_RING_1:def 1;
hence thesis;
end;
thus for k st k in dom g holds h.:(len f + k)=g.:k
proof
let k; assume A6:k in dom g;
then A7:0<>k & k<=len g by FINSEQ_3:27;
then 0<>len f+k & len f+k<=len f+len g by NAT_1:23,REAL_1:55;
then h.:(len f + k)=h.(len f+k) by A2,O_RING_1:def 1
.=g.k by A1,A6,FINSEQ_1:def 7
.=g.:k by A7,O_RING_1:def 1;
hence thesis;
end;
end;
thus (dom h = Seg(len f + len g) &
(for k st k in dom f holds h.:k=f.:k) &
(for k st k in dom g holds h.:(len f + k)=g.:k)) implies
h=f^g
proof
assume that
A8:dom h = Seg(len f + len g) and
A9:for k st k in dom f holds h.:k=f.:k and
A10:for k st k in dom g holds h.:(len f + k)=g.:k;
A11:len h=len f+len g by A8,FINSEQ_1:def 3;
A12:for k st k in dom f holds h.k=f.k
proof
let k such that A13:k in dom f;
A14:len f<=len f+len g by NAT_1:29;
A15:0<>k & k<=len f by A13,FINSEQ_3:27;
then 0<>k & k<=len h by A11,A14,AXIOMS:22;
then h.k=h.:k by O_RING_1:def 1
.=f.:k by A9,A13
.=f.k by A15,O_RING_1:def 1;
hence thesis;
end;
for k st k in dom g holds h.(len f + k)=g.k
proof
let k; assume A16:k in dom g;
then A17:0<>k & k<=len g by FINSEQ_3:27;
then 0<>len f+k & len f+k<=len f+len g by NAT_1:23,REAL_1:55;
then h.(len f + k)=h.:(len f+k) by A11,O_RING_1:def 1
.=g.:k by A10,A16
.=g.k by A17,O_RING_1:def 1;
hence thesis;
end;
hence h=f^g by A8,A12,FINSEQ_1:def 7;
end;
end;
Lm5:
f=<*x*> iff len f =1 & f.:1=x
proof
thus f=<*x*> implies len f=1 & f.:1=x
proof
assume A1:f=<*x*>;
hence len f=1 by FINSEQ_1:57;
then f.:1=f.1 by O_RING_1:def 1
.=x by A1,FINSEQ_1:57;
hence thesis;
end;
thus len f=1 & f.:1=x implies f=<*x*>
proof
assume that
A2:len f=1 and
A3:f.:1=x;
f.1=x by A2,A3,O_RING_1:def 1;
hence thesis by A2,FINSEQ_1:57;
end;
end;
Lm6:
(f^<*x*>).:(len f + 1)=x
proof
len f+1=len f+len<*x*> by FINSEQ_1:56
.=len(f^<*x*>) by FINSEQ_1:35;
then 0<>len f+1 & len f+1<=len(f^<*x*>) by NAT_1:21;
then (f^<*x*>).:(len f+1)=(f^<*x*>).(len f+1) by O_RING_1:def 1
.=x by FINSEQ_1:59;
hence thesis;
end;
Lm7:
i<>0 & i<=len f implies (f^g).:i=f.:i
proof
assume i<>0 & i<=len f;
then 0<>i & 0<=i & i<=len f by NAT_1:18;
then 0<i & i<=len f by REAL_1:def 5;
then 0+1<=i & i<=len f by NAT_1:38;
then i in dom f by FINSEQ_3:27;
hence thesis by Lm4;
end;
Lm8:
i<>0 & i<=len g implies (f^g).:(len f+i)=g.:i
proof
assume i<>0 & i<=len g;
then 0<>i & 0<=i & i<=len g by NAT_1:18;
then 0<i & i<=len g by REAL_1:def 5;
then 0+1<=i & i<=len g by NAT_1:38;
then i in dom g by FINSEQ_3:27;
hence thesis by Lm4;
end;
Lm9:
x is_a_square implies <*x*> is_a_Product_of_squares
proof
assume A1:x is_a_square;
A2: len<*x*>=1 by Lm5;
A3:<*x*>.:1 is_a_square by A1,Lm5;
for n st n<>0 & n<len <*x*>
ex y st y is_a_square & <*x*>.:(n+1)=<*x*>.:n*y
proof
let n; assume n<>0 & n<len <*x*>;
then n<>0 & n<1 by Lm5;
hence thesis by Lm1;
end;
hence thesis by A2,A3,O_RING_1:def 6;
end;
Lm10:
x is_a_square implies x is_a_product_of_squares
proof
assume x is_a_square;
then A1:<*x*> is_a_Product_of_squares by Lm9;
len<*x*>=1 & <*x*>.:1=x by Lm5;
hence thesis by A1,O_RING_1:def 7;
end;
Lm11:
x is_a_square implies <*x*> is_an_Amalgam_of_squares
proof
assume x is_a_square;
then A1:x is_a_product_of_squares by Lm10;
A2: len<*x*>=1 by Lm5;
A3:<*x*>.:1 is_a_product_of_squares by A1,Lm5;
for n st n<>0 & n<=len <*x*> holds <*x*>.:n is_a_product_of_squares or
ex i,j st <*x*>.:n=<*x*>.:i*<*x*>.:j & i<>0 & i<n & j<>0 & j<n
proof
let n; assume n<>0 & n<=len <*x*>;
then n<>0 & n<=1 by Lm5;
hence thesis by A3,Lm3;
end;
hence thesis by A2,O_RING_1:def 10;
end;
Lm12:
x is_a_square implies x is_an_amalgam_of_squares
proof
assume x is_a_square;
then A1:<*x*> is_an_Amalgam_of_squares by Lm11;
len<*x*>=1 & <*x*>.:1=x by Lm5;
hence thesis by A1,O_RING_1:def 11;
end;
Lm13:
f is_an_Amalgam_of_squares & g is_an_Amalgam_of_squares
implies f^g is_an_Amalgam_of_squares
proof
assume A1:f is_an_Amalgam_of_squares & g is_an_Amalgam_of_squares;
then len f<>0 by O_RING_1:def 10;
then len f+len g<>0 by NAT_1:23;
then A2:len(f^g)<>0 by FINSEQ_1:35;
for n st n<>0 & n<=len (f^g) holds (f^g).:n is_a_product_of_squares or
ex i,j st (f^g).:n=(f^g).:i*(f^g).:j & i<>0 & i<n & j<>0 & j<n
proof
let n; assume A3:n<>0 & n<=len (f^g);
then A4:n<=len f+len g by FINSEQ_1:35;
A5:now assume A6:n<=len f;
then A7: f.:n is_a_product_of_squares implies thesis by A3,Lm7;
now given k,l such that
A8:f.:n=f.:k*f.:l & k<>0 & k<n & l<>0 & l<n;
A9: k<=len f by A6,A8,AXIOMS:22;
A10: l<=len f by A6,A8,AXIOMS:22;
(f^g).:n=f.:k*f.:l by A3,A6,A8,Lm7
.=(f^g).:k*f.:l by A8,A9,Lm7
.=(f^g).:k*(f^g).:l by A8,A10,Lm7;
hence thesis by A8;
end;
hence thesis by A1,A3,A6,A7,O_RING_1:def 10;
end;
now assume A11: len f<n;
then consider m such that A12:n=len f+m by NAT_1:28;
A13:m<=len g by A4,A12,REAL_1:53;
m<>0 & len f+m<=len f+len g by A3,A11,A12,FINSEQ_1:35;
then A14:m<>0 & m<=len g by REAL_1:53;
then A15: g.:
m is_a_product_of_squares implies thesis by A12,Lm8;
now given k,l such that
A16:g.:m=g.:k*g.:l & k<>0 & k<m & l<>0 & l<m;
A17:k<>0 & k<=len g by A13,A16,AXIOMS:22;
A18:l<>0 & l<=len g by A13,A16,AXIOMS:22;
A19:(f^g).:n=g.:k*g.:l by A12,A14,A16,Lm8
.=(f^g).:(len f+k)*g.:l by A17,Lm8
.=(f^g).:(len f+k)*(f^g).:(len f+l)
by A18,Lm8;
A20:len f+k<>0 & len f+l<>0 by A16,NAT_1:23;
len f+k<n & len f+l<n by A12,A16,REAL_1:53;
hence thesis by A19,A20;
end;
hence thesis
by A1,A14,A15,O_RING_1:def 10;
end;
hence thesis by A5;
end;
hence thesis by A2,O_RING_1:def 10;
end;
Lm14:
f is_a_generation_from_squares & g is_a_generation_from_squares
implies f^g is_a_generation_from_squares
proof
assume that
A1:f is_a_generation_from_squares and
A2:g is_a_generation_from_squares;
len f<>0 by A1,O_RING_1:def 14;
then len f+len g<>0 by NAT_1:23;
then A3:len(f^g)<>0 by FINSEQ_1:35;
for n st n<>0 & n<=len (f^g) holds (f^g).:n is_an_amalgam_of_squares or
ex i,j st ((f^g).:n=(f^g).:i*(f^g).:j or (f^g).:n=(f^g).:i+(f^g).:j) &
i<>0 & i<n & j<>0 & j<n
proof
let n; assume A4:n<>0 & n<=len (f^g);
then A5:n<=len f+len g by FINSEQ_1:35;
A6:now assume A7:n<=len f;
then A8:(f^g).:n=f.:n by A4,Lm7;
A9: f.:n is_an_amalgam_of_squares implies thesis by A4,A7,Lm7;
now given k,l such that
A10:(f.:n=f.:k*f.:l or f.:n=f.:k+f.:l) &
k<>0 & k<n & l<>0 & l<n;
k<=len f by A7,A10,AXIOMS:22;
then A11:(f^g).:k=f.:k by A10,Lm7;
l<=len f by A7,A10,AXIOMS:22;
then (f^g).:l=f.:l by A10,Lm7;
hence thesis by A8,A10,A11;
end;
hence thesis by A1,A4,A7,A9,O_RING_1:def 14;
end;
now assume A12: len f<n;
then consider m such that A13:n=len f+m by NAT_1:28;
A14:m<=len g by A5,A13,REAL_1:53;
m<>0 & len f+m<=len f+len g by A4,A12,A13,FINSEQ_1:35;
then A15:m<>0 & m<=len g by REAL_1:53;
then A16: g.:
m is_an_amalgam_of_squares implies thesis by A13,Lm8
;
now given k,l such that
A17:(g.:m=g.:k*g.:l or g.:m=g.:k+g.:
l) & k<>0 & k<m & l<>0 & l<m;
A18:k<>0 & k<=len g by A14,A17,AXIOMS:22;
A19:l<>0 & l<=len g by A14,A17,AXIOMS:22;
A20:(f^g).:n=(f^g).:(len f+k)*(f^g).:(len f+l) or
(f^g).:n=(f^g).:(len f+k)+(f^g).:(len f+l)
proof
A21:now assume g.:m=g.:k*g.:l;
then (f^g).:n=g.:k*g.:l by A13,A15,Lm8
.=(f^g).:(len f+k)*g.:l by A18,Lm8
.=(f^g).:(len f+k)*(f^g).:(len f+l)
by A19,Lm8;
hence thesis;
end;
now assume g.:m=g.:k+g.:l;
then (f^g).:n=g.:k+g.:l by A13,A15,Lm8
.=(f^g).:(len f+k)+g.:l by A18,Lm8
.=(f^g).:(len f+k)+(f^g).:(len f+l)
by A19,Lm8;
hence thesis;
end;
hence thesis by A17,A21;
end;
A22:len f+k<>0 & len f+l<>0 by A17,NAT_1:23;
len f+k<n & len f+l<n by A13,A17,REAL_1:53;
hence thesis by A20,A22;
end;
hence thesis by A2,A15,A16,O_RING_1:def 14;
end;
hence thesis by A6;
end;
hence thesis by A3,O_RING_1:def 14;
end;
Lm15:
f is_a_generation_from_squares & x is_a_square
implies f^<*x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares & x is_a_square;
then len f<>0 by O_RING_1:def 14;
then len f+len<*x*><>0 by NAT_1:23;
then A2:len (f^<*x*>)<>0 by FINSEQ_1:35;
set g=f^<*x*>;
A3:len g=len f+len<*x*> by FINSEQ_1:35
.=len f+1 by Lm5;
for n st n<>0 & n<=len g holds
g.:n is_an_amalgam_of_squares or
ex i,j st (g.:n=g.:i*g.:j or g.:n=g.:i+g.:
j) & i<>0 & i<n & j<>0 & j<n
proof
let n such that A4:n<>0 & n<=len g;
A5:now assume n<len g;
then A6:n<=len f by A3,NAT_1:38;
then A7:g.:n=f.:n by A4,Lm7;
A8: f.:n is_an_amalgam_of_squares implies thesis by A4,A6,Lm7;
now given k,m such that
A9:(f.:n=f.:k*f.:m or f.:n=f.:k+f.:m) & k<>0 & k<n & m<>0 &
m<n;
k<=len f by A6,A9,AXIOMS:22;
then A10:f.:k=g.:k by A9,Lm7;
m<=len f by A6,A9,AXIOMS:22;
then f.:m=g.:m by A9,Lm7;
hence thesis by A7,A9,A10;
end;
hence thesis
by A1,A4,A6,A8,O_RING_1:def 14;
end;
now assume n=len g;
then g.:n=x by A3,Lm6;
hence thesis by A1,Lm12;
end;
hence thesis by A4,A5,REAL_1:def 5;
end;
hence thesis by A2,O_RING_1:def 14;
end;
Lm16:
f is_a_generation_from_squares & x is_an_amalgam_of_squares
implies f^<*x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares &
x is_an_amalgam_of_squares;
then len f<>0 by O_RING_1:def 14;
then len f+len<*x*><>0 by NAT_1:23;
then A2:len (f^<*x*>)<>0 by FINSEQ_1:35;
set g=f^<*x*>;
A3:len g=len f+len<*x*> by FINSEQ_1:35
.=len f+1 by Lm5;
for n st n<>0 & n<=len g holds
g.:n is_an_amalgam_of_squares or
ex i,j st (g.:n=g.:i*g.:j or g.:n=g.:i+g.:
j) & i<>0 & i<n & j<>0 & j<n
proof
let n such that A4:n<>0 & n<=len g;
A5:now assume n<len g;
then A6:n<=len f by A3,NAT_1:38;
then A7:g.:n=f.:n by A4,Lm7;
A8: f.:n is_an_amalgam_of_squares implies thesis by A4,A6,Lm7;
now given k,m such that
A9:(f.:n=f.:k*f.:m or f.:n=f.:k+f.:m) & k<>0 & k<n & m<>0 &
m<n;
k<=len f by A6,A9,AXIOMS:22;
then A10:f.:k=g.:k by A9,Lm7;
m<=len f by A6,A9,AXIOMS:22;
then f.:m=g.:m by A9,Lm7;
hence thesis by A7,A9,A10;
end;
hence thesis by A1,A4,A6,A8,O_RING_1:def 14;
end;
n=len g implies thesis by A1,A3,Lm6;
hence thesis by A4,A5,REAL_1:def 5;
end;
hence thesis by A2,O_RING_1:def 14;
end;
Lm17:
f is_an_Amalgam_of_squares & i<>0 & i<=len f & j<>0 & j<=len f
implies f^<*f.:i*f.:j*> is_an_Amalgam_of_squares
proof
assume A1:f is_an_Amalgam_of_squares & i<>0 & i<=len f & j<>0 &
j<=len f;
then len f<>0 by O_RING_1:def 10;
then len f+len<*f.:i*f.:j*><>0 by NAT_1:23;
then A2:len (f^<*f.:i*f.:j*>)<>0 by FINSEQ_1:35;
set g=f^<*f.:i*f.:j*>;
A3:len g=len f+len<*f.:i*f.:j*> by FINSEQ_1:35
.=len f+1 by Lm5;
for n st n<>0 & n<=len g holds
g.:n is_a_product_of_squares or
ex i,j st g.:n=g.:i*g.:j & i<>0 & i<n & j<>0 & j<n
proof
let n such that A4:n<>0 & n<=len g;
A5:now assume n<len g;
then A6:n<=len f by A3,NAT_1:38;
then A7: f.:n is_a_product_of_squares implies thesis by A4,Lm7;
now given k,m such that
A8:f.:n=f.:k*f.:m & k<>0 & k<n & m<>0 & m<n;
A9: k<=len f by A6,A8,AXIOMS:22;
A10: m<=len f by A6,A8,AXIOMS:22;
g.:n=f.:k*f.:m by A4,A6,A8,Lm7
.=g.:k*f.:m by A8,A9,Lm7
.=g.:k*g.:m by A8,A10,Lm7;
hence thesis by A8;
end;
hence thesis by A1,A4,A6,A7,O_RING_1:def 10;
end;
now assume A11: n=len g;
then g.:n=f.:i*f.:j by A3,Lm6
.=g.:i*f.:j by A1,Lm7
.=g.:i*g.:j by A1,Lm7;
then g.:n=g.:i*g.:j & i<n & j<n by A1,A3,A11,NAT_1:38;
hence thesis by A1;
end;
hence thesis by A4,A5,REAL_1:def 5;
end;
hence thesis by A2,O_RING_1:def 10;
end;
Lm18:
f is_a_generation_from_squares & i<>0 & i<=len f & j<>0 & j<=len f
implies f^<*f.:i*f.:j*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares &
i<>0 & i<=len f & j<>0 & j<=len f;
then len f<>0 by O_RING_1:def 14;
then len f+len<*f.:i*f.:j*><>0 by NAT_1:23;
then A2:len (f^<*f.:i*f.:j*>)<>0 by FINSEQ_1:35;
set g=f^<*f.:i*f.:j*>;
A3:len g=len f+len<*f.:i*f.:j*> by FINSEQ_1:35
.=len f+1 by Lm5;
for n st n<>0 & n<=len g holds
g.:n is_an_amalgam_of_squares or
ex i,j st (g.:n=g.:i*g.:j or g.:n=g.:i+g.:
j) & i<>0 & i<n & j<>0 & j<n
proof
let n such that A4:n<>0 & n<=len g;
A5:now assume n<len g;
then A6:n<=len f by A3,NAT_1:38;
then A7:g.:n=f.:n by A4,Lm7;
A8: f.:n is_an_amalgam_of_squares implies thesis by A4,A6,Lm7;
now given k,m such that
A9:(f.:n=f.:k*f.:m or f.:n=f.:k+f.:m) & k<>0 & k<n & m<>0 &
m<n;
k<=len f by A6,A9,AXIOMS:22;
then A10:f.:k=g.:k by A9,Lm7;
m<=len f by A6,A9,AXIOMS:22;
then f.:m=g.:m by A9,Lm7;
hence thesis by A7,A9,A10;
end;
hence thesis by A1,A4,A6,A8,O_RING_1:def 14;
end;
now assume A11: n=len g;
then g.:n=f.:i*f.:j by A3,Lm6
.=g.:i*f.:j by A1,Lm7
.=g.:i*g.:j by A1,Lm7;
then g.:n=g.:i*g.:j & i<n & j<n by A1,A3,A11,NAT_1:38;
hence thesis by A1;
end;
hence thesis by A4,A5,REAL_1:def 5;
end;
hence thesis by A2,O_RING_1:def 14;
end;
Lm19:
f is_a_Product_of_squares & x is_a_square
implies f^<*f.:len f*x*> is_a_Product_of_squares
proof
assume that
A1:f is_a_Product_of_squares and
A2:x is_a_square;
set g=f^<*f.:len f*x*>;
A3:len g=len f+len <*f.:len f*x*> by FINSEQ_1:35
.=len f+1 by Lm5;
then A4:len g<>0 by NAT_1:21;
A5:for n st n<>0 & n<len g holds f.:n=g.:n
proof
let n; assume n<>0 & n<len g;
then 1<=n & n<=len f by A3,Lm2,NAT_1:38;
then n in dom f by FINSEQ_3:27;
hence thesis by Lm4;
end;
len f<>0 by A1,O_RING_1:def 6;
then 1<=len f by Lm2;
then 1<>0 & 1<len g by A3,NAT_1:38;
then g.:1=f.:1 by A5;
then A6:g.:1 is_a_square by A1,O_RING_1:def 6;
for n st n<>0 & n<len g ex y st y is_a_square & g.:(n+1)=g.:n*y
proof
let n; assume A7:n<>0 & n<len g;
then A8:n<=len f by A3,NAT_1:38;
A9:now assume A10:n<len f;
A11:f.:n=g.:n by A5,A7;
n+1<>0 & n+1<len g by A3,A10,NAT_1:21,REAL_1:53
;
then f.:(n+1)=g.:(n+1) by A5;
hence thesis by A1,A7,A10,A11,O_RING_1:def 6;
end;
now assume A12:n=len f;
then A13:g.:(n+1)=f.:n*x by Lm6;
1<=n & n<=len f by A7,A12,Lm2;
then n in dom f by FINSEQ_3:27;
then g.:(n+1)=g.:n*x by A13,Lm4;
hence thesis by A2;
end;
hence thesis by A8,A9,REAL_1:def 5;
end;
hence thesis by A4,A6,O_RING_1:def 6;
end;
Lm20:
f is_a_generation_from_squares & x is_a_square
implies (f^<*x*>)^<*f.:len f*x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares & x is_a_square;
then A2:f^<*x*> is_a_generation_from_squares by Lm15;
A3:len<*x*>=1 by Lm5;
A4:len f<>0 by A1,O_RING_1:def 14;
A5: len f<=len f+1 by NAT_1:29;
A6: len f+1<>0 & len f+1=len(f^<*x*>) by A3,FINSEQ_1:35,NAT_1:21;
A7:(f^<*x*>).:len f=f.:len f by A4,Lm7;
(f^<*x*>).:(len f+1)=x by Lm6;
hence thesis by A2,A4,A5,A6,A7,Lm18;
end;
Lm21:
f is_a_generation_from_squares & x is_an_amalgam_of_squares
implies (f^<*x*>)^<*f.:len f*x*> is_a_generation_from_squares
proof
assume A1:f is_a_generation_from_squares &
x is_an_amalgam_of_squares;
then A2:f^<*x*> is_a_generation_from_squares by Lm16;
A3:len<*x*>=1 by Lm5;
A4:len f<>0 by A1,O_RING_1:def 14;
A5: len f<=len f+1 by NAT_1:29;
A6: len f+1<>0 & len f+1=len(f^<*x*>) by A3,FINSEQ_1:35,NAT_1:21;
A7:(f^<*x*>).:len f=f.:len f by A4,Lm7;
(f^<*x*>).:(len f+1)=x by Lm6;
hence thesis by A2,A4,A5,A6,A7,Lm18;
end;
Lm22:
f is_an_Amalgam_of_squares & g is_an_Amalgam_of_squares
implies (f^g)^<*f.:len f*g.:len g*> is_an_Amalgam_of_squares
proof
assume that
A1:f is_an_Amalgam_of_squares and
A2:g is_an_Amalgam_of_squares;
A3:len f<>0 & len f<=len f by A1,O_RING_1:def 10;
len f<>0 & len f<=len f+len g by A1,NAT_1:29,O_RING_1:def 10;
then A4:len f<>0 & len f<=len(f^g) by FINSEQ_1:35;
A5:len g<>0 & len g<=len g by A2,O_RING_1:def 10;
then A6:len f+len g<>0 & len f+len g<=len(f^g) by FINSEQ_1:35,NAT_1:23;
A7:(f^g).:len f=f.:len f by A3,Lm7;
A8:(f^g).:(len f+len g)=g.:len g by A5,Lm8;
f^g is_an_Amalgam_of_squares by A1,A2,Lm13;
hence thesis by A4,A6,A7,A8,Lm17;
end;
Lm23:
f is_a_generation_from_squares & g is_a_generation_from_squares
implies (f^g)^<*f.:len f*g.:len g*> is_a_generation_from_squares
proof
assume that
A1:f is_a_generation_from_squares and
A2:g is_a_generation_from_squares;
A3:(f^g) is_a_generation_from_squares by A1,A2,Lm14;
A4:len f<>0 by A1,O_RING_1:def 14;
len f<=len f+len g by NAT_1:29;
then A5:len f<>0 & len f<=len(f^g) by A1,FINSEQ_1:35,O_RING_1:def 14;
A6:len g<>0 by A2,O_RING_1:def 14;
then A7:len f+len g<>0 & len f+len g<=len(f^g) by FINSEQ_1:35,NAT_1:23;
1<=len f & len f<=len f by A4,Lm2;
then len f in dom f by FINSEQ_3:27;
then A8:(f^g).:len f=f.:len f by Lm4;
1<=len g & len g<=len g by A6,Lm2;
then len g in dom g by FINSEQ_3:27;
then (f^g).:(len f+len g)=g.:len g by Lm4;
hence thesis by A3,A5,A7,A8,Lm18;
end;
theorem
x is_a_square & y is_a_square
implies x*y is_a_product_of_squares
proof
assume that
A1:x is_a_square and
A2:y is_a_square;
x is_a_product_of_squares by A1,O_RING_1:1;
then consider f such that A3:f is_a_Product_of_squares & x=f.:len f
by O_RING_1:def 7;
take g=f^<*x*y*>;
len g=len f+len <*x*y*> by FINSEQ_1:35
.=len f+1 by Lm5;
hence thesis by A2,A3,Lm6,Lm19;
end;
theorem
x is_a_product_of_squares & y is_a_square
implies x*y is_a_product_of_squares
proof
assume that
A1:x is_a_product_of_squares and
A2:y is_a_square;
consider f such that A3:f is_a_Product_of_squares & x=f.:len f
by A1,O_RING_1:def 7;
take g=f^<*x*y*>;
len g=len f+len <*x*y*> by FINSEQ_1:35
.=len f+1 by Lm5;
hence thesis by A2,A3,Lm6,Lm19;
end;
Lm24:
x is_a_square & y is_a_product_of_squares
implies x*y is_an_amalgam_of_squares
proof
assume that
A1:x is_a_square and
A2:y is_a_product_of_squares;
A3:x is_an_amalgam_of_squares by A1,O_RING_1:1;
A4:y is_an_amalgam_of_squares by A2,O_RING_1:3;
consider f such that
A5:f is_an_Amalgam_of_squares & x=f.:len f
by A3,O_RING_1:def 11;
consider g such that
A6:g is_an_Amalgam_of_squares & y=g.:len g
by A4,O_RING_1:def 11;
take h=(f^g)^<*f.:len f*g.:len g*>;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
hence thesis by A5,A6,Lm6,Lm22;
end;
Lm25:
x is_a_square & y is_an_amalgam_of_squares
implies x*y is_an_amalgam_of_squares
proof
assume that
A1:x is_a_square and
A2:y is_an_amalgam_of_squares;
x is_an_amalgam_of_squares by A1,O_RING_1:1;
then consider f such that
A3:f is_an_Amalgam_of_squares & x=f.:len f
by O_RING_1:def 11;
consider g such that
A4:g is_an_Amalgam_of_squares & y=g.:len g
by A2,O_RING_1:def 11;
take h=(f^g)^<*f.:len f*g.:len g*>;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
hence thesis by A3,A4,Lm6,Lm22;
end;
theorem
x is_a_square & y is_a_product_of_squares or
x is_a_square & y is_an_amalgam_of_squares
implies x*y is_an_amalgam_of_squares
by Lm24,Lm25;
Lm26:
x is_a_product_of_squares & y is_a_product_of_squares
implies x*y is_an_amalgam_of_squares
proof
assume that
A1:x is_a_product_of_squares and
A2:y is_a_product_of_squares;
A3:x is_an_amalgam_of_squares by A1,O_RING_1:3;
A4:y is_an_amalgam_of_squares by A2,O_RING_1:3;
consider f such that
A5:f is_an_Amalgam_of_squares & x=f.:len f
by A3,O_RING_1:def 11;
consider g such that
A6:g is_an_Amalgam_of_squares & y=g.:len g
by A4,O_RING_1:def 11;
take h=(f^g)^<*f.:len f*g.:len g*>;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
hence thesis by A5,A6,Lm6,Lm22;
end;
Lm27:
x is_a_product_of_squares & y is_an_amalgam_of_squares
implies x*y is_an_amalgam_of_squares
proof
assume that
A1:x is_a_product_of_squares and
A2:y is_an_amalgam_of_squares;
x is_an_amalgam_of_squares by A1,O_RING_1:3;
then consider f such that
A3:f is_an_Amalgam_of_squares & x=f.:len f
by O_RING_1:def 11;
consider g such that
A4:g is_an_Amalgam_of_squares & y=g.:len g
by A2,O_RING_1:def 11;
take h=(f^g)^<*f.:len f*g.:len g*>;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
hence thesis by A3,A4,Lm6,Lm22;
end;
theorem
x is_a_product_of_squares & y is_a_product_of_squares or
x is_a_product_of_squares & y is_an_amalgam_of_squares
implies x*y is_an_amalgam_of_squares
by Lm26,Lm27;
Lm28:
x is_an_amalgam_of_squares & y is_a_square
implies x*y is_an_amalgam_of_squares
proof
assume that
A1:x is_an_amalgam_of_squares and
A2:y is_a_square;
A3:y is_an_amalgam_of_squares by A2,O_RING_1:1;
consider f such that
A4:f is_an_Amalgam_of_squares & x=f.:len f
by A1,O_RING_1:def 11;
consider g such that
A5:g is_an_Amalgam_of_squares & y=g.:len g
by A3,O_RING_1:def 11;
take h=(f^g)^<*f.:len f*g.:len g*>;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
hence thesis by A4,A5,Lm6,Lm22;
end;
Lm29:
x is_an_amalgam_of_squares & y is_a_product_of_squares
implies x*y is_an_amalgam_of_squares
proof
assume that
A1:x is_an_amalgam_of_squares and
A2:y is_a_product_of_squares;
A3:y is_an_amalgam_of_squares by A2,O_RING_1:3;
consider f such that
A4:f is_an_Amalgam_of_squares & x=f.:len f
by A1,O_RING_1:def 11;
consider g such that
A5:g is_an_Amalgam_of_squares & y=g.:len g
by A3,O_RING_1:def 11;
take h=(f^g)^<*f.:len f*g.:len g*>;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
hence thesis by A4,A5,Lm6,Lm22;
end;
Lm30:
x is_an_amalgam_of_squares & y is_an_amalgam_of_squares
implies x*y is_an_amalgam_of_squares
proof
assume that
A1:x is_an_amalgam_of_squares and
A2:y is_an_amalgam_of_squares;
consider f such that
A3:f is_an_Amalgam_of_squares & x=f.:len f
by A1,O_RING_1:def 11;
consider g such that
A4:g is_an_Amalgam_of_squares & y=g.:len g
by A2,O_RING_1:def 11;
take h=(f^g)^<*f.:len f*g.:len g*>;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
hence thesis by A3,A4,Lm6,Lm22;
end;
theorem
x is_an_amalgam_of_squares & y is_a_square or
x is_an_amalgam_of_squares & y is_a_product_of_squares or
x is_an_amalgam_of_squares & y is_an_amalgam_of_squares
implies x*y is_an_amalgam_of_squares
by Lm28,Lm29,Lm30;
Lm31:
x is_a_square & y is_a_sum_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_square and
A2:y is_a_sum_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:1;
A4:y is_generated_from_squares by A2,O_RING_1:2;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm32:
x is_a_square & y is_a_sum_of_products_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_square and
A2:y is_a_sum_of_products_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:1;
A4:y is_generated_from_squares by A2,O_RING_1:4;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm33:
x is_a_square & y is_a_sum_of_amalgams_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_square and
A2:y is_a_sum_of_amalgams_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:1;
A4:y is_generated_from_squares by A2,O_RING_1:6;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm34:
x is_a_square & y is_generated_from_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_square and
A2:y is_generated_from_squares;
x is_generated_from_squares by A1,O_RING_1:1;
then consider f such that
A3:f is_a_generation_from_squares and
A4:x=f.:len f
by O_RING_1:def 15;
consider g such that
A5:g is_a_generation_from_squares and
A6:y=g.:len g
by A2,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A7:h is_a_generation_from_squares by A3,A5,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A4,Lm6;
hence thesis by A6,A7,O_RING_1:def 15;
end;
theorem
x is_a_square & y is_a_sum_of_squares or
x is_a_square & y is_a_sum_of_products_of_squares or
x is_a_square & y is_a_sum_of_amalgams_of_squares or
x is_a_square & y is_generated_from_squares
implies x*y is_generated_from_squares
by Lm31,Lm32,Lm33,Lm34;
Lm35:
x is_a_sum_of_squares & y is_a_square
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_squares and
A2:y is_a_square;
A3:x is_generated_from_squares by A1,O_RING_1:2;
A4:y is_generated_from_squares by A2,O_RING_1:1;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm36:
x is_a_sum_of_squares & y is_a_sum_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_squares and
A2:y is_a_sum_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:2;
A4:y is_generated_from_squares by A2,O_RING_1:2;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm37:
x is_a_sum_of_squares & y is_a_product_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_squares and
A2:y is_a_product_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:2;
A4:y is_generated_from_squares by A2,O_RING_1:3;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm38:
x is_a_sum_of_squares & y is_a_sum_of_products_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_squares and
A2:y is_a_sum_of_products_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:2;
A4:y is_generated_from_squares by A2,O_RING_1:4;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm39:
x is_a_sum_of_squares & y is_an_amalgam_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_squares and
A2:y is_an_amalgam_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:2;
A4:y is_generated_from_squares by A2,O_RING_1:5;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm40:
x is_a_sum_of_squares & y is_a_sum_of_amalgams_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_squares and
A2:y is_a_sum_of_amalgams_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:2;
A4:y is_generated_from_squares by A2,O_RING_1:6;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm41:
x is_a_sum_of_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_squares and
A2:y is_generated_from_squares;
x is_generated_from_squares by A1,O_RING_1:2;
then consider f such that
A3:f is_a_generation_from_squares and
A4:x=f.:len f
by O_RING_1:def 15;
consider g such that
A5:g is_a_generation_from_squares and
A6:y=g.:len g
by A2,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A7:h is_a_generation_from_squares by A3,A5,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A4,Lm6;
hence thesis by A6,A7,O_RING_1:def 15;
end;
theorem
x is_a_sum_of_squares & y is_a_square or
x is_a_sum_of_squares & y is_a_sum_of_squares or
x is_a_sum_of_squares & y is_a_product_of_squares or
x is_a_sum_of_squares & y is_a_sum_of_products_of_squares or
x is_a_sum_of_squares & y is_an_amalgam_of_squares or
x is_a_sum_of_squares & y is_a_sum_of_amalgams_of_squares or
x is_a_sum_of_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
by Lm35,Lm36,Lm37,Lm38,Lm39,Lm40,Lm41;
Lm42:
x is_a_product_of_squares & y is_a_sum_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_product_of_squares and
A2:y is_a_sum_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:3;
A4:y is_generated_from_squares by A2,O_RING_1:2;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm43:
x is_a_product_of_squares & y is_a_sum_of_products_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_product_of_squares and
A2:y is_a_sum_of_products_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:3;
A4:y is_generated_from_squares by A2,O_RING_1:4;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm44:
x is_a_product_of_squares & y is_a_sum_of_amalgams_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_product_of_squares and
A2:y is_a_sum_of_amalgams_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:3;
A4:y is_generated_from_squares by A2,O_RING_1:6;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm45:
x is_a_product_of_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_product_of_squares and
A2:y is_generated_from_squares;
x is_generated_from_squares by A1,O_RING_1:3;
then consider f such that
A3:f is_a_generation_from_squares and
A4:x=f.:len f
by O_RING_1:def 15;
consider g such that
A5:g is_a_generation_from_squares and
A6:y=g.:len g
by A2,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A7:h is_a_generation_from_squares by A3,A5,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A4,Lm6;
hence thesis by A6,A7,O_RING_1:def 15;
end;
theorem
x is_a_product_of_squares & y is_a_sum_of_squares or
x is_a_product_of_squares & y is_a_sum_of_products_of_squares or
x is_a_product_of_squares & y is_a_sum_of_amalgams_of_squares or
x is_a_product_of_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
by Lm42,Lm43,Lm44,Lm45;
Lm46:
x is_a_sum_of_products_of_squares & y is_a_square
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_products_of_squares and
A2:y is_a_square;
A3:x is_generated_from_squares by A1,O_RING_1:4;
A4:y is_generated_from_squares by A2,O_RING_1:1;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm47:
x is_a_sum_of_products_of_squares & y is_a_sum_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_products_of_squares and
A2:y is_a_sum_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:4;
A4:y is_generated_from_squares by A2,O_RING_1:2;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm48:
x is_a_sum_of_products_of_squares & y is_a_product_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_products_of_squares and
A2:y is_a_product_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:4;
A4:y is_generated_from_squares by A2,O_RING_1:3;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm49:
x is_a_sum_of_products_of_squares & y is_a_sum_of_products_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_products_of_squares and
A2:y is_a_sum_of_products_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:4;
A4:y is_generated_from_squares by A2,O_RING_1:4;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm50:
x is_a_sum_of_products_of_squares & y is_an_amalgam_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_products_of_squares and
A2:y is_an_amalgam_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:4;
A4:y is_generated_from_squares by A2,O_RING_1:5;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm51:
x is_a_sum_of_products_of_squares & y is_a_sum_of_amalgams_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_products_of_squares and
A2:y is_a_sum_of_amalgams_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:4;
A4:y is_generated_from_squares by A2,O_RING_1:6;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm52:
x is_a_sum_of_products_of_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_products_of_squares and
A2:y is_generated_from_squares;
x is_generated_from_squares by A1,O_RING_1:4;
then consider f such that
A3:f is_a_generation_from_squares and
A4:x=f.:len f
by O_RING_1:def 15;
consider g such that
A5:g is_a_generation_from_squares and
A6:y=g.:len g
by A2,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A7:h is_a_generation_from_squares by A3,A5,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A4,Lm6;
hence thesis by A6,A7,O_RING_1:def 15;
end;
theorem
x is_a_sum_of_products_of_squares & y is_a_square or
x is_a_sum_of_products_of_squares & y is_a_sum_of_squares or
x is_a_sum_of_products_of_squares & y is_a_product_of_squares or
x is_a_sum_of_products_of_squares & y is_a_sum_of_products_of_squares or
x is_a_sum_of_products_of_squares & y is_an_amalgam_of_squares or
x is_a_sum_of_products_of_squares & y is_a_sum_of_amalgams_of_squares or
x is_a_sum_of_products_of_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
by Lm46,Lm47,Lm48,Lm49,Lm50,Lm51,Lm52;
Lm53:
x is_an_amalgam_of_squares & y is_a_sum_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_an_amalgam_of_squares and
A2:y is_a_sum_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:5;
A4:y is_generated_from_squares by A2,O_RING_1:2;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm54:
x is_an_amalgam_of_squares & y is_a_sum_of_products_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_an_amalgam_of_squares and
A2:y is_a_sum_of_products_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:5;
A4:y is_generated_from_squares by A2,O_RING_1:4;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm55:
x is_an_amalgam_of_squares & y is_a_sum_of_amalgams_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_an_amalgam_of_squares and
A2:y is_a_sum_of_amalgams_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:5;
A4:y is_generated_from_squares by A2,O_RING_1:6;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm56:
x is_an_amalgam_of_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_an_amalgam_of_squares and
A2:y is_generated_from_squares;
x is_generated_from_squares by A1,O_RING_1:5;
then consider f such that
A3:f is_a_generation_from_squares and
A4:x=f.:len f
by O_RING_1:def 15;
consider g such that
A5:g is_a_generation_from_squares and
A6:y=g.:len g
by A2,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A7:h is_a_generation_from_squares by A3,A5,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A4,Lm6;
hence thesis by A6,A7,O_RING_1:def 15;
end;
theorem
x is_an_amalgam_of_squares & y is_a_sum_of_squares or
x is_an_amalgam_of_squares & y is_a_sum_of_products_of_squares or
x is_an_amalgam_of_squares & y is_a_sum_of_amalgams_of_squares or
x is_an_amalgam_of_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
by Lm53,Lm54,Lm55,Lm56;
Lm57:
x is_a_sum_of_amalgams_of_squares & y is_a_square
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_amalgams_of_squares and
A2:y is_a_square;
A3:x is_generated_from_squares by A1,O_RING_1:6;
A4:y is_generated_from_squares by A2,O_RING_1:1;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm58:
x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_amalgams_of_squares and
A2:y is_a_sum_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:6;
A4:y is_generated_from_squares by A2,O_RING_1:2;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm59:
x is_a_sum_of_amalgams_of_squares & y is_a_product_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_amalgams_of_squares and
A2:y is_a_product_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:6;
A4:y is_generated_from_squares by A2,O_RING_1:3;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm60:
x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_products_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_amalgams_of_squares and
A2:y is_a_sum_of_products_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:6;
A4:y is_generated_from_squares by A2,O_RING_1:4;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm61:
x is_a_sum_of_amalgams_of_squares & y is_an_amalgam_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_amalgams_of_squares and
A2:y is_an_amalgam_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:6;
A4:y is_generated_from_squares by A2,O_RING_1:5;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares
by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm62:
x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_amalgams_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_amalgams_of_squares and
A2:y is_a_sum_of_amalgams_of_squares;
A3:x is_generated_from_squares by A1,O_RING_1:6;
A4:y is_generated_from_squares by A2,O_RING_1:6;
consider f such that
A5:f is_a_generation_from_squares and
A6:x=f.:len f
by A3,O_RING_1:def 15;
consider g such that
A7:g is_a_generation_from_squares and
A8:y=g.:len g
by A4,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A9:h is_a_generation_from_squares by A5,A7,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A6,Lm6;
hence thesis by A8,A9,O_RING_1:def 15;
end;
Lm63:
x is_a_sum_of_amalgams_of_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_a_sum_of_amalgams_of_squares and
A2:y is_generated_from_squares;
x is_generated_from_squares by A1,O_RING_1:6;
then consider f such that
A3:f is_a_generation_from_squares and
A4:x=f.:len f
by O_RING_1:def 15;
consider g such that
A5:g is_a_generation_from_squares and
A6:y=g.:len g
by A2,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A7:h is_a_generation_from_squares by A3,A5,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A4,Lm6;
hence thesis by A6,A7,O_RING_1:def 15;
end;
theorem
x is_a_sum_of_amalgams_of_squares & y is_a_square or
x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_squares or
x is_a_sum_of_amalgams_of_squares & y is_a_product_of_squares or
x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_products_of_squares or
x is_a_sum_of_amalgams_of_squares & y is_an_amalgam_of_squares or
x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_amalgams_of_squares or
x is_a_sum_of_amalgams_of_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
by Lm57,Lm58,Lm59,Lm60,Lm61,Lm62,Lm63;
Lm64:
x is_generated_from_squares & y is_a_square
implies x*y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_a_square;
consider f such that
A3:f is_a_generation_from_squares & x=f.:len f
by A1,O_RING_1:def 15;
take g=(f^<*y*>)^<*f.:len f*y*>;
len g=len(f^<*y*>)+len<*f.:len f*y*> by FINSEQ_1:35
.=len(f^<*y*>)+1 by Lm5;
hence thesis by A2,A3,Lm6,Lm20;
end;
Lm65:
x is_generated_from_squares & y is_an_amalgam_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_an_amalgam_of_squares;
consider f such that
A3:f is_a_generation_from_squares & x=f.:len f
by A1,O_RING_1:def 15;
take g=(f^<*y*>)^<*f.:len f*y*>;
len g=len(f^<*y*>)+len<*f.:len f*y*> by FINSEQ_1:35
.=len(f^<*y*>)+1 by Lm5;
hence thesis by A2,A3,Lm6,Lm21;
end;
Lm66:
x is_generated_from_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_generated_from_squares;
consider f such that
A3:f is_a_generation_from_squares and
A4:x=f.:len f
by A1,O_RING_1:def 15;
consider g such that
A5:g is_a_generation_from_squares and
A6:y=g.:len g
by A2,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A7:h is_a_generation_from_squares by A3,A5,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A4,Lm6;
hence thesis by A6,A7,O_RING_1:def 15;
end;
Lm67:
x is_generated_from_squares & y is_a_sum_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_a_sum_of_squares;
A3:y is_generated_from_squares by A2,O_RING_1:2;
consider f such that
A4:f is_a_generation_from_squares and
A5:x=f.:len f
by A1,O_RING_1:def 15;
consider g such that
A6:g is_a_generation_from_squares and
A7:y=g.:len g
by A3,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A8:h is_a_generation_from_squares by A4,A6,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A5,Lm6;
hence thesis by A7,A8,O_RING_1:def 15;
end;
Lm68:
x is_generated_from_squares & y is_a_product_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_a_product_of_squares;
A3:y is_generated_from_squares by A2,O_RING_1:3;
consider f such that
A4:f is_a_generation_from_squares and
A5:x=f.:len f
by A1,O_RING_1:def 15;
consider g such that
A6:g is_a_generation_from_squares and
A7:y=g.:len g
by A3,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A8:h is_a_generation_from_squares by A4,A6,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A5,Lm6;
hence thesis by A7,A8,O_RING_1:def 15;
end;
Lm69:
x is_generated_from_squares & y is_a_sum_of_products_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_a_sum_of_products_of_squares;
A3:y is_generated_from_squares by A2,O_RING_1:4;
consider f such that
A4:f is_a_generation_from_squares and
A5:x=f.:len f
by A1,O_RING_1:def 15;
consider g such that
A6:g is_a_generation_from_squares and
A7:y=g.:len g
by A3,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A8:h is_a_generation_from_squares by A4,A6,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A5,Lm6;
hence thesis by A7,A8,O_RING_1:def 15;
end;
Lm70:
x is_generated_from_squares & y is_a_sum_of_amalgams_of_squares
implies x*y is_generated_from_squares
proof
assume that
A1:x is_generated_from_squares and
A2:y is_a_sum_of_amalgams_of_squares;
A3:y is_generated_from_squares by A2,O_RING_1:6;
consider f such that
A4:f is_a_generation_from_squares and
A5:x=f.:len f
by A1,O_RING_1:def 15;
consider g such that
A6:g is_a_generation_from_squares and
A7:y=g.:len g
by A3,O_RING_1:def 15;
set h=(f^g)^<*f.:len f*g.:len g*>;
A8:h is_a_generation_from_squares by A4,A6,Lm23;
len h=len(f^g)+len<*f.:len f*g.:len g*> by FINSEQ_1:35
.=len(f^g)+1 by Lm5;
then h.:len h=x*g.:len g by A5,Lm6;
hence thesis by A7,A8,O_RING_1:def 15;
end;
theorem
x is_generated_from_squares & y is_a_square or
x is_generated_from_squares & y is_a_sum_of_squares or
x is_generated_from_squares & y is_a_product_of_squares or
x is_generated_from_squares & y is_a_sum_of_products_of_squares or
x is_generated_from_squares & y is_an_amalgam_of_squares or
x is_generated_from_squares & y is_a_sum_of_amalgams_of_squares or
x is_generated_from_squares & y is_generated_from_squares
implies x*y is_generated_from_squares
by Lm64,Lm65,Lm66,Lm67,Lm68,Lm69,Lm70;