set A = the addF of H;
reconsider P = rng f as Preserv of the addF of H by Lm2;
reconsider Z = 0. H as Element of P by Lm1;
take addLoopStr(# P,( the addF of H || P),Z #) ; :: thesis: ( the carrier of addLoopStr(# P,( the addF of H || P),Z #) = rng f & the addF of addLoopStr(# P,( the addF of H || P),Z #) = the addF of H || (rng f) & the ZeroF of addLoopStr(# P,( the addF of H || P),Z #) = 0. H )
thus ( the carrier of addLoopStr(# P,( the addF of H || P),Z #) = rng f & the addF of addLoopStr(# P,( the addF of H || P),Z #) = the addF of H || (rng f) & the ZeroF of addLoopStr(# P,( the addF of H || P),Z #) = 0. H ) ; :: thesis: verum