set C1 = [#] K;
A1: ( 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) #);
( 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
A2: 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 A2; :: 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 b1 being Element of the carrier of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) st b1 * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) )
assume A3: x <> 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) ; :: thesis: ex b1 being Element of the carrier of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) st b1 * 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 A3, ALGSTR_0:def 39;
then consider v being Element of K such that
A4: v * x1 = 1. K ;
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 A4; :: thesis: verum
end;
thus not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated ; :: 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 A1, Th2;
hence ex b1 being Subfield of K st b1 is strict ; :: thesis: verum