take ModuleStr(# (n -tuples_on the carrier of R),(vector_add (n,R)),(n |-> (0. R)),(vector_mult (n,R)) #) ; :: thesis: ( the carrier of ModuleStr(# (n -tuples_on the carrier of R),(vector_add (n,R)),(n |-> (0. R)),(vector_mult (n,R)) #) = n -tuples_on the carrier of R & the addF of ModuleStr(# (n -tuples_on the carrier of R),(vector_add (n,R)),(n |-> (0. R)),(vector_mult (n,R)) #) = vector_add (n,R) & the ZeroF of ModuleStr(# (n -tuples_on the carrier of R),(vector_add (n,R)),(n |-> (0. R)),(vector_mult (n,R)) #) = n |-> (0. R) & the lmult of ModuleStr(# (n -tuples_on the carrier of R),(vector_add (n,R)),(n |-> (0. R)),(vector_mult (n,R)) #) = vector_mult (n,R) )
thus ( the carrier of ModuleStr(# (n -tuples_on the carrier of R),(vector_add (n,R)),(n |-> (0. R)),(vector_mult (n,R)) #) = n -tuples_on the carrier of R & the addF of ModuleStr(# (n -tuples_on the carrier of R),(vector_add (n,R)),(n |-> (0. R)),(vector_mult (n,R)) #) = vector_add (n,R) & the ZeroF of ModuleStr(# (n -tuples_on the carrier of R),(vector_add (n,R)),(n |-> (0. R)),(vector_mult (n,R)) #) = n |-> (0. R) & the lmult of ModuleStr(# (n -tuples_on the carrier of R),(vector_add (n,R)),(n |-> (0. R)),(vector_mult (n,R)) #) = vector_mult (n,R) ) ; :: thesis: verum