set C1 = [#] K;
P0: ( the addF of K = the addF of K || ([#] K) & the multF of K = the multF of K || ([#] K) ) by RELSET_1:19;
set ST = doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #);
P4: ( 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 0. K & 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 1. K ) ;
( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is right_complementable & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated )

proof

thus doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is right_complementable :: thesis: ( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated )

proof

let x be Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x1 = x as Element of K ;
consider v being Element of K such that
A1: x1 + v = 0. K by ALGSTR_0:def 11;
reconsider y = v as Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #)
thus x + y = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) by A1; :: thesis: verum

end;

thus doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative :: thesis: ( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated )

proof

let x, y be Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #); :: according to GROUP_1:def 12 :: thesis: x * y = y * x
reconsider x1 = x, y1 = y as Element of K ;
( x * y = x1 * y1 & y * x = y1 * x1 ) ;
hence x * y = y * x ; :: thesis: verum

end;

thus doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible :: thesis: not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated

proof

let x be Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #); :: according to VECTSP_1:def 9 :: thesis: ( x = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) or ex b₁ being Element of the carrier of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) st b₁ * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) )
assume A2: x <> 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ; :: thesis: ex b₁ being Element of the carrier of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) st b₁ * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #)
reconsider x1 = x as Element of K ;
x1 is left_invertible by A2, ALGSTR_0:def 39;
then consider v being Element of K such that
A3: v * x1 = 1. K by ALGSTR_0:def 27;
reconsider y = v as Element of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ;
take y ; :: thesis: y * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #)
thus y * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) by A3; :: thesis: verum

end;

( 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 0. K & 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) = 1. K & 0. K <> 1. K ) ;
hence not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated by STRUCT_0:def 8; :: thesis: verum

end;

then doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is Subfield of K by P0, P4, PF2;
hence ex b₁ being Subfield of K st b₁ is strict ; :: thesis: verum