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);
now :: thesis: for x being object st x in Bags X holds
((1. L) | (X,L)) . x = (1_ (X,L)) . x
set m = (0_ (X,L)) +* ((EmptyBag X),(1. L));
let x be object ; :: thesis: ( x in Bags X implies ((1. L) | (X,L)) . b1 = (1_ (X,L)) . b1 )
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)) . b1 = (1_ (X,L)) . b1
then reconsider x9 = x as bag of X ;
A1: dom (0_ (X,L)) = dom ((Bags X) --> (0. L)) by POLYNOM1:def 8
.= Bags X ;
then A2: m = (0_ (X,L)) +* ((EmptyBag X) .--> (1. L)) by FUNCT_7:def 3;
A3: EmptyBag X in dom ((EmptyBag X) .--> (1. L)) by TARSKI:def 1;
A4: m . (EmptyBag X) = ((0_ (X,L)) +* ((EmptyBag X) .--> (1. L))) . (EmptyBag X) by A1, FUNCT_7:def 3
.= ((EmptyBag X) .--> (1. L)) . (EmptyBag X) by A3, FUNCT_4:13
.= 1. L by FUNCOP_1:72 ;
per cases ( x9 = EmptyBag X or x9 <> EmptyBag X ) ;
suppose x9 = EmptyBag X ; :: thesis: ((1. L) | (X,L)) . b1 = (1_ (X,L)) . b1
hence ((1. L) | (X,L)) . x = (1_ (X,L)) . x by A4, POLYNOM1:25; :: thesis: verum
end;
suppose A5: x9 <> EmptyBag X ; :: thesis: ((1. L) | (X,L)) . b1 = (1_ (X,L)) . b1
then not x9 in dom ((EmptyBag X) .--> (1. L)) by TARSKI:def 1;
then m . x9 = (0_ (X,L)) . x9 by A2, FUNCT_4:11
.= 0. L by POLYNOM1:22
.= (1_ (X,L)) . x9 by A5, POLYNOM1:25 ;
hence ((1. L) | (X,L)) . x = (1_ (X,L)) . x ; :: thesis: verum
end;
end;
end;
hence (1. L) | (X,L) = 1_ (X,L) ; :: thesis: verum