let A, B be Ordinal-Sequence; :: thesis: for b being Ordinal holds b -leading_coeff (A ^ B) = (b -leading_coeff A) ^ (b -leading_coeff B)
let b be Ordinal; :: thesis: b -leading_coeff (A ^ B) = (b -leading_coeff A) ^ (b -leading_coeff B)
A1: dom (b -leading_coeff (A ^ B)) = dom (A ^ B) by Def3
.= (dom A) +^ (dom B) by ORDINAL4:def 1
.= (dom A) +^ (dom (b -leading_coeff B)) by Def3
.= (dom (b -leading_coeff A)) +^ (dom (b -leading_coeff B)) by Def3
.= dom ((b -leading_coeff A) ^ (b -leading_coeff B)) by ORDINAL4:def 1 ;

now :: thesis: for x being object st x in dom (b -leading_coeff (A ^ B)) holds
(b -leading_coeff (A ^ B)) . x = ((b -leading_coeff A) ^ (b -leading_coeff B)) . x

let x be object ; :: thesis: ( x in dom (b -leading_coeff (A ^ B)) implies (b -leading_coeff (A ^ B)) . b₁ = ((b -leading_coeff A) ^ (b -leading_coeff B)) . b₁ )
assume x in dom (b -leading_coeff (A ^ B)) ; :: thesis: (b -leading_coeff (A ^ B)) . b₁ = ((b -leading_coeff A) ^ (b -leading_coeff B)) . b₁
then A2: x in dom (A ^ B) by Def3;
then A3: (b -leading_coeff (A ^ B)) . x = b -leading_coeff ((A ^ B) . x) by Def3;
reconsider c = x as Ordinal by A2;
( c in dom A or ( dom A c= c & c -^ (dom A) in dom B ) )

proof

assume not c in dom A ; :: thesis: ( dom A c= c & c -^ (dom A) in dom B )
hence A4: dom A c= c by ORDINAL1:16; :: thesis: c -^ (dom A) in dom B
c in (dom A) +^ (dom B) by A2, ORDINAL4:def 1;
then c -^ (dom A) in ((dom A) +^ (dom B)) -^ (dom A) by A4, ORDINAL3:53;
hence c -^ (dom A) in dom B by ORDINAL3:52; :: thesis: verum

end;

per cases then ( c in dom A or ( dom A c= c & c -^ (dom A) in dom B ) ) ;

suppose A5: c in dom A ; :: thesis: (b -leading_coeff (A ^ B)) . b₁ = ((b -leading_coeff A) ^ (b -leading_coeff B)) . b₁

then A6: c in dom (b -leading_coeff A) by Def3;
(A ^ B) . x = A . x by A5, ORDINAL4:def 1;
hence (b -leading_coeff (A ^ B)) . x = (b -leading_coeff A) . x by A3, A5, Def3
.= ((b -leading_coeff A) ^ (b -leading_coeff B)) . x by A6, ORDINAL4:def 1 ;
:: thesis: verum

end;

suppose A7: ( dom A c= c & c -^ (dom A) in dom B ) ; :: thesis: (b -leading_coeff (A ^ B)) . b₁ = ((b -leading_coeff A) ^ (b -leading_coeff B)) . b₁

then A8: c -^ (dom A) in dom (b -leading_coeff B) by Def3;
(A ^ B) . x = (A ^ B) . ((dom A) +^ (c -^ (dom A))) by A7, ORDINAL3:def 5
.= B . (c -^ (dom A)) by A7, ORDINAL4:def 1 ;
hence (b -leading_coeff (A ^ B)) . x = (b -leading_coeff B) . (c -^ (dom A)) by A3, A7, Def3
.= ((b -leading_coeff A) ^ (b -leading_coeff B)) . ((dom (b -leading_coeff A)) +^ (c -^ (dom A))) by A8, ORDINAL4:def 1
.= ((b -leading_coeff A) ^ (b -leading_coeff B)) . ((dom A) +^ (c -^ (dom A))) by Def3
.= ((b -leading_coeff A) ^ (b -leading_coeff B)) . x by A7, ORDINAL3:def 5 ;
:: thesis: verum

end;

end;

end;

hence b -leading_coeff (A ^ B) = (b -leading_coeff A) ^ (b -leading_coeff B) by A1, FUNCT_1:2; :: thesis: verum