let V1 be free finite-rank Z_Module; :: thesis: for p2 being FinSequence of V1
for p1 being FinSequence of INT.Ring st dom p1 = dom p2 holds
dom (lmlt (p1,p2)) = dom p1
let p2 be FinSequence of V1; :: thesis: for p1 being FinSequence of INT.Ring st dom p1 = dom p2 holds
dom (lmlt (p1,p2)) = dom p1
let p1 be FinSequence of INT.Ring; :: thesis: ( dom p1 = dom p2 implies dom (lmlt (p1,p2)) = dom p1 )
assume A1: dom p1 = dom p2 ; :: thesis: dom (lmlt (p1,p2)) = dom p1
A2: [:(rng p1),(rng p2):] c= [:INT, the carrier of V1:] by ZFMISC_1:96;
A3: ( rng <:p1,p2:> c= [:(rng p1),(rng p2):] & [:INT, the carrier of V1:] = dom the lmult of V1 ) by FUNCT_2:def 1, FUNCT_3:51;
thus dom (lmlt (p1,p2)) = dom ( the lmult of V1 * <:p1,p2:>) by FUNCOP_1:def 3
.= dom <:p1,p2:> by A2, A3, RELAT_1:27, XBOOLE_1:1
.= (dom p1) /\ (dom p2) by FUNCT_3:def 7
.= dom p1 by A1 ; :: thesis: verum