reconsider o = X --> (0. L) as Element of Funcs (X, the carrier of L) by FUNCT_2:8;
take ModuleStr(# (Funcs (X, the carrier of L)),(mapAdd (X,L)),o,(mapMult (X,L)) #) ; :: thesis: ( the carrier of ModuleStr(# (Funcs (X, the carrier of L)),(mapAdd (X,L)),o,(mapMult (X,L)) #) = Funcs (X, the carrier of L) & the addF of ModuleStr(# (Funcs (X, the carrier of L)),(mapAdd (X,L)),o,(mapMult (X,L)) #) = mapAdd (X,L) & the ZeroF of ModuleStr(# (Funcs (X, the carrier of L)),(mapAdd (X,L)),o,(mapMult (X,L)) #) = X --> (0. L) & the lmult of ModuleStr(# (Funcs (X, the carrier of L)),(mapAdd (X,L)),o,(mapMult (X,L)) #) = mapMult (X,L) )
thus ( the carrier of ModuleStr(# (Funcs (X, the carrier of L)),(mapAdd (X,L)),o,(mapMult (X,L)) #) = Funcs (X, the carrier of L) & the addF of ModuleStr(# (Funcs (X, the carrier of L)),(mapAdd (X,L)),o,(mapMult (X,L)) #) = mapAdd (X,L) & the ZeroF of ModuleStr(# (Funcs (X, the carrier of L)),(mapAdd (X,L)),o,(mapMult (X,L)) #) = X --> (0. L) & the lmult of ModuleStr(# (Funcs (X, the carrier of L)),(mapAdd (X,L)),o,(mapMult (X,L)) #) = mapMult (X,L) ) ; :: thesis: verum