theorem lift6b: :: FIELD_12:38

for F1, F2 being Field st F1 == F2 holds
( 0_. F1 = 0_. F2 & 1_. F1 = 1_. F2 )