let L be non empty right_complementable add-associative right_zeroed associative commutative well-unital distributive 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 6;
A2: len <%y%> <= 1 by ALGSEQ_1:def 6;

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 Th35;
hence contradiction by A3, POLYNOM4:6; :: thesis: verum

end;

then x * y <> 0. L by VECTSP_2:def 5;
then A4: len <%(x * y)%> = 1 by Th34;
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 11;
1 in dom r by A5, FINSEQ_3:27;
then r . 1 = (<%x%> . (1 -' 1)) * (<%y%> . ((0 + 1) -' 1)) by A7
.= (<%x%> . 0 ) * (<%y%> . (1 -' 1)) by XREAL_1:234
.= (<%x%> . 0 ) * (<%y%> . 0 ) by XREAL_1:234
.= (<%x%> . 0 ) * y by ALGSEQ_1:def 6
.= x * y by ALGSEQ_1:def 6 ;
then A8: r = <*(x * y)*> by A5, FINSEQ_1:57;

A9: now

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:61
.= <%(x * y)%> . n by A10, ALGSEQ_1:def 6 ;
:: 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 5;
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:13;
hence <%x%> *' <%y%> = <%(x * y)%> by A9, A4, ALGSEQ_1:28; :: thesis: verum

end;

suppose A13: len <%x%> = 0 ; :: thesis: <%x%> *' <%y%> = <%(x * y)%>

then A14: x = 0. L by Th34;
<%x%> = 0_. L by A13, POLYNOM4:8;
hence <%x%> *' <%y%> = 0_. L by POLYNOM4:5
.= <%(0. L)%> by Th35
.= <%(x * y)%> by A14, VECTSP_1:39 ;
:: thesis: verum

end;

suppose A15: len <%y%> = 0 ; :: thesis: <%x%> *' <%y%> = <%(x * y)%>

then A16: y = 0. L by Th34;
<%y%> = 0_. L by A15, POLYNOM4:8;
hence <%x%> *' <%y%> = 0_. L by POLYNOM3:35
.= <%(0. L)%> by Th35
.= <%(x * y)%> by A16, VECTSP_1:39 ;
:: thesis: verum

end;

end;