let Q be multLoop; :: thesis: for x, y being Element of Q holds
( x * (lp (Nucl Q)) = y * (lp (Nucl Q)) iff ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) )
let x, y be Element of Q; :: thesis: ( x * (lp (Nucl Q)) = y * (lp (Nucl Q)) iff ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) )
thus ( x * (lp (Nucl Q)) = y * (lp (Nucl Q)) implies ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) ) :: thesis: ( ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) implies x * (lp (Nucl Q)) = y * (lp (Nucl Q)) )

proof

assume A1: x * (lp (Nucl Q)) = y * (lp (Nucl Q)) ; :: thesis: ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) )
A2: 1. Q in Nucl Q by Th20;
y = (1. Q) * (y * (1. Q)) ;
hence ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) by Th60, A1, A2; :: thesis: verum

end;

given u, v being Element of Q such that A3: ( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) ; :: thesis: x * (lp (Nucl Q)) = y * (lp (Nucl Q))
A4: ( u in Nucl_l Q & u in Nucl_m Q ) by A3, Th12;
A5: ( v in Nucl_m Q & v in Nucl_r Q ) by A3, Th12;
for w being Element of Q holds
( w in x * (lp (Nucl Q)) iff w in y * (lp (Nucl Q)) )

proof

let w be Element of Q; :: thesis: ( w in x * (lp (Nucl Q)) iff w in y * (lp (Nucl Q)) )
thus ( w in x * (lp (Nucl Q)) implies w in y * (lp (Nucl Q)) ) :: thesis: ( w in y * (lp (Nucl Q)) implies w in x * (lp (Nucl Q)) )

proof

assume w in x * (lp (Nucl Q)) ; :: thesis: w in y * (lp (Nucl Q))
then consider u1, v1 being Element of Q such that
A6: ( u1 in Nucl Q & v1 in Nucl Q & w = u1 * (x * v1) ) by Th60;
ex u2, v2 being Element of Q st
( u2 in Nucl Q & v2 in Nucl Q & w = u2 * (y * v2) )

proof

take u1 / u ; :: thesis: ex v2 being Element of Q st
( u1 / u in Nucl Q & v2 in Nucl Q & w = (u1 / u) * (y * v2) )
take v \ v1 ; :: thesis: ( u1 / u in Nucl Q & v \ v1 in Nucl Q & w = (u1 / u) * (y * (v \ v1)) )
( u in [#] (lp (Nucl Q)) & u1 in [#] (lp (Nucl Q)) ) by A3, A6, Th24;
then u1 / u in [#] (lp (Nucl Q)) by Th41;
hence u1 / u in Nucl Q by Th24; :: thesis: ( v \ v1 in Nucl Q & w = (u1 / u) * (y * (v \ v1)) )
( v in [#] (lp (Nucl Q)) & v1 in [#] (lp (Nucl Q)) ) by A3, A6, Th24;
then v \ v1 in [#] (lp (Nucl Q)) by Th39;
hence v \ v1 in Nucl Q by Th24; :: thesis: w = (u1 / u) * (y * (v \ v1))
w = u1 * (x * (v * (v \ v1))) by A6
.= ((u1 / u) * u) * ((x * v) * (v \ v1)) by Def23, A5
.= (u1 / u) * (u * ((x * v) * (v \ v1))) by Def23, A4
.= (u1 / u) * (y * (v \ v1)) by A3, Def22, A4 ;
hence w = (u1 / u) * (y * (v \ v1)) ; :: thesis: verum

end;

hence w in y * (lp (Nucl Q)) by Th60; :: thesis: verum

end;

thus ( w in y * (lp (Nucl Q)) implies w in x * (lp (Nucl Q)) ) :: thesis: verum

proof

assume w in y * (lp (Nucl Q)) ; :: thesis: w in x * (lp (Nucl Q))
then consider u1, v1 being Element of Q such that
A7: ( u1 in Nucl Q & v1 in Nucl Q & w = u1 * (y * v1) ) by Th60;
ex u2, v2 being Element of Q st
( u2 in Nucl Q & v2 in Nucl Q & w = u2 * (x * v2) )

proof

take u1 * u ; :: thesis: ex v2 being Element of Q st
( u1 * u in Nucl Q & v2 in Nucl Q & w = (u1 * u) * (x * v2) )
take v * v1 ; :: thesis: ( u1 * u in Nucl Q & v * v1 in Nucl Q & w = (u1 * u) * (x * (v * v1)) )
( u in [#] (lp (Nucl Q)) & u1 in [#] (lp (Nucl Q)) ) by A3, A7, Th24;
then u1 * u in [#] (lp (Nucl Q)) by Th37;
hence u1 * u in Nucl Q by Th24; :: thesis: ( v * v1 in Nucl Q & w = (u1 * u) * (x * (v * v1)) )
( v in [#] (lp (Nucl Q)) & v1 in [#] (lp (Nucl Q)) ) by A3, A7, Th24;
then v * v1 in [#] (lp (Nucl Q)) by Th37;
hence v * v1 in Nucl Q by Th24; :: thesis: w = (u1 * u) * (x * (v * v1))
w = u1 * (((u * x) * v) * v1) by A3, A7, Def24, A5
.= u1 * ((u * x) * (v * v1)) by Def23, A5
.= u1 * (u * (x * (v * v1))) by Def22, A4
.= (u1 * u) * (x * (v * v1)) by Def23, A4 ;
hence w = (u1 * u) * (x * (v * v1)) ; :: thesis: verum

end;

hence w in x * (lp (Nucl Q)) by Th60; :: thesis: verum

end;

end;

hence x * (lp (Nucl Q)) = y * (lp (Nucl Q)) by SUBSET_1:3; :: thesis: verum