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 & 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 A2: ( len <%x%> <> 0 & len <%y%> <> 0 ) ; :: thesis: <%x%> *' <%y%> = <%(x * y)%>

then ( len <%x%> >= 0 + 1 & len <%y%> >= 0 + 1 ) by NAT_1:13;
then A4: ( len <%x%> = 1 & len <%y%> = 1 ) by A1, XXREAL_0:1;
( <%x%> . ((len <%x%>) -' 1) <> 0. L & <%y%> . ((len <%y%>) -' 1) <> 0. L ) by A2, Lm2;
then (<%x%> . ((len <%x%>) -' 1)) * (<%y%> . ((len <%y%>) -' 1)) <> 0. L by VECTSP_2:def 5;
then A5: len (<%x%> *' <%y%>) = (1 + 1) - 1 by A4, POLYNOM4:13;
consider r being FinSequence of the carrier of L such that
A6: len r = 0 + 1 and
A7: (<%x%> *' <%y%>) . 0 = Sum r and
A8: 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 A6, FINSEQ_3:27;
then r . 1 = (<%x%> . (1 -' 1)) * (<%y%> . ((0 + 1) -' 1)) by A8
.= (<%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 A9: r = <*(x * y)*> by A6, FINSEQ_1:57;

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

end;

( 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 A2, POLYNOM4:6; :: thesis: verum

end;

then x * y <> 0. L by VECTSP_2:def 5;
then len <%(x * y)%> = 1 by Th34;
hence <%x%> *' <%y%> = <%(x * y)%> by A5, A10, ALGSEQ_1:28; :: thesis: verum

end;

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

then A13: <%x%> = 0_. L by POLYNOM4:8;
A14: x = 0. L by A12, Th34;
thus <%x%> *' <%y%> = 0_. L by A13, 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 POLYNOM4:8;
A17: y = 0. L by A15, Th34;
thus <%x%> *' <%y%> = 0_. L by A16, POLYNOM3:35
.= <%(0. L)%> by Th35
.= <%(x * y)%> by A17, VECTSP_1:39 ; :: thesis: verum

end;

end;