let L be non empty right_complementable add-associative right_zeroed well-unital distributive associative commutative domRing-like doubleLoopStr ; :: thesis: for x, y being Element of L holds <%x%> *' <%y%> = <%(x * y)%>
let x, y be Element of L; :: thesis: <%x%> *' <%y%> = <%(x * y)%>
A1: len <%x%> <= 1 by ALGSEQ_1:def 5;
A2: len <%y%> <= 1 by ALGSEQ_1:def 5;
per cases ( ( len <%x%> <> 0 & len <%y%> <> 0 ) or len <%x%> = 0 or len <%y%> = 0 ) ;
suppose A3: ( len <%x%> <> 0 & len <%y%> <> 0 ) ; :: thesis: <%x%> *' <%y%> = <%(x * y)%>
( x <> 0. L & y <> 0. L )
proof
assume ( x = 0. L or y = 0. L ) ; :: thesis: contradiction
then ( <%x%> = 0_. L or <%y%> = 0_. L ) by Th34;
hence contradiction by A3, POLYNOM4:3; :: thesis: verum
end;
then x * y <> 0. L by VECTSP_2:def 1;
then A4: len <%(x * y)%> = 1 by Th33;
consider r being FinSequence of the carrier of L such that
A5: len r = 0 + 1 and
A6: (<%x%> *' <%y%>) . 0 = Sum r and
A7: for k being Element of NAT st k in dom r holds
r . k = (<%x%> . (k -' 1)) * (<%y%> . ((0 + 1) -' k)) by POLYNOM3:def 9;
1 in dom r by A5, FINSEQ_3:25;
then r . 1 = (<%x%> . (1 -' 1)) * (<%y%> . ((0 + 1) -' 1)) by A7
.= (<%x%> . 0) * (<%y%> . (1 -' 1)) by XREAL_1:232
.= (<%x%> . 0) * (<%y%> . 0) by XREAL_1:232
.= (<%x%> . 0) * y by ALGSEQ_1:def 5
.= x * y by ALGSEQ_1:def 5 ;
then A8: r = <*(x * y)*> by A5, FINSEQ_1:40;
A9: now :: thesis: for n being Nat st n < 1 holds
(<%x%> *' <%y%>) . n = <%(x * y)%> . n
let n be Nat; :: thesis: ( n < 1 implies (<%x%> *' <%y%>) . n = <%(x * y)%> . n )
assume n < 1 ; :: thesis: (<%x%> *' <%y%>) . n = <%(x * y)%> . n
then n < 0 + 1 ;
then A10: n = 0 by NAT_1:13;
hence (<%x%> *' <%y%>) . n = x * y by A6, A8, RLVECT_1:44
.= <%(x * y)%> . n by A10, ALGSEQ_1:def 5 ;
:: thesis: verum
end;
( <%x%> . ((len <%x%>) -' 1) <> 0. L & <%y%> . ((len <%y%>) -' 1) <> 0. L ) by A3, Lm2;
then A11: (<%x%> . ((len <%x%>) -' 1)) * (<%y%> . ((len <%y%>) -' 1)) <> 0. L by VECTSP_2:def 1;
len <%y%> >= 0 + 1 by A3, NAT_1:13;
then A12: len <%y%> = 1 by A2, XXREAL_0:1;
len <%x%> >= 0 + 1 by A3, NAT_1:13;
then len <%x%> = 1 by A1, XXREAL_0:1;
then len (<%x%> *' <%y%>) = (1 + 1) - 1 by A12, A11, POLYNOM4:10;
hence <%x%> *' <%y%> = <%(x * y)%> by A9, A4, ALGSEQ_1:12; :: thesis: verum
end;
suppose A13: len <%x%> = 0 ; :: thesis: <%x%> *' <%y%> = <%(x * y)%>
then A14: x = 0. L by Th33;
<%x%> = 0_. L by A13, POLYNOM4:5;
hence <%x%> *' <%y%> = 0_. L by POLYNOM4:2
.= <%(0. L)%> by Th34
.= <%(x * y)%> by A14 ;
:: thesis: verum
end;
suppose A15: len <%y%> = 0 ; :: thesis: <%x%> *' <%y%> = <%(x * y)%>
then A16: y = 0. L by Th33;
<%y%> = 0_. L by A15, POLYNOM4:5;
hence <%x%> *' <%y%> = 0_. L by POLYNOM3:34
.= <%(0. L)%> by Th34
.= <%(x * y)%> by A16 ;
:: thesis: verum
end;
end;