let X be set ; :: thesis: for L being non empty well-unital multLoopStr_0 holds (1. L) | X,L = 1_ X,L
let L be non empty well-unital multLoopStr_0 ; :: thesis: (1. L) | X,L = 1_ X,L
set o1 = (1. L) | X,L;
set o2 = 1_ X,L;

A1: now

set m = (0_ X,L) +* (EmptyBag X),(1. L);
let x be set ; :: thesis: ( x in Bags X implies ((1. L) | X,L) . b₁ = (1_ X,L) . b₁ )
reconsider m = (0_ X,L) +* (EmptyBag X),(1. L) as Function of (Bags X),the carrier of L ;
reconsider m = m as Function of (Bags X),L ;
reconsider m = m as Series of X,L ;
assume x in Bags X ; :: thesis: ((1. L) | X,L) . b₁ = (1_ X,L) . b₁
then reconsider x9 = x as bag of X ;
A2: dom (0_ X,L) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 24
.= Bags X by FUNCOP_1:19 ;
then A3: m = (0_ X,L) +* ((EmptyBag X) .--> (1. L)) by FUNCT_7:def 3;
A4: dom ((EmptyBag X) .--> (1. L)) = {(EmptyBag X)} by FUNCOP_1:19;
then A5: EmptyBag X in dom ((EmptyBag X) .--> (1. L)) by TARSKI:def 1;
A6: m . (EmptyBag X) = ((0_ X,L) +* ((EmptyBag X) .--> (1. L))) . (EmptyBag X) by A2, FUNCT_7:def 3
.= ((EmptyBag X) .--> (1. L)) . (EmptyBag X) by A5, FUNCT_4:14
.= 1. L by FUNCOP_1:87 ;

per cases ( x9 = EmptyBag X or x9 <> EmptyBag X ) ;

suppose x9 = EmptyBag X ; :: thesis: ((1. L) | X,L) . b₁ = (1_ X,L) . b₁

hence ((1. L) | X,L) . x = (1_ X,L) . x by A6, POLYNOM1:84; :: thesis: verum

end;

suppose A7: x9 <> EmptyBag X ; :: thesis: ((1. L) | X,L) . b₁ = (1_ X,L) . b₁

then not x9 in dom ((EmptyBag X) .--> (1. L)) by A4, TARSKI:def 1;
then m . x9 = (0_ X,L) . x9 by A3, FUNCT_4:12
.= 0. L by POLYNOM1:81
.= (1_ X,L) . x9 by A7, POLYNOM1:84 ;
hence ((1. L) | X,L) . x = (1_ X,L) . x ; :: thesis: verum

end;

end;

end;

( Bags X = dom ((1. L) | X,L) & Bags X = dom (1_ X,L) ) by FUNCT_2:def 1;
hence (1. L) | X,L = 1_ X,L by A1, FUNCT_1:9; :: thesis: verum