begin
theorem
canceled;
theorem Th2:
:: deftheorem Def1 defines FS2XFS PRGCOR_2:def 1 :
:: deftheorem defines XFS2FS PRGCOR_2:def 2 :
theorem Th3:
theorem Th4:
:: deftheorem Def3 defines FS2XFS* PRGCOR_2:def 3 :
:: deftheorem Def4 defines XFS2FS* PRGCOR_2:def 4 :
theorem Th5:
:: deftheorem Def5 defines is_an_xrep_of PRGCOR_2:def 5 :
theorem
:: deftheorem Def6 defines IFLGT PRGCOR_2:def 6 :
for
x,
y,
a,
b,
c being
set holds
( (
x in y implies
IFLGT x,
y,
a,
b,
c = a ) & (
x = y implies
IFLGT x,
y,
a,
b,
c = b ) & ( not
x in y & not
x = y implies
IFLGT x,
y,
a,
b,
c = c ) );
theorem Th7:
:: deftheorem Def7 defines inner_prd_prg PRGCOR_2:def 7 :
theorem Th8:
theorem
theorem
:: deftheorem Def8 defines scalar_prd_prg PRGCOR_2:def 8 :
theorem
:: deftheorem Def9 defines vector_minus_prg PRGCOR_2:def 9 :
theorem
:: deftheorem Def10 defines vector_add_prg PRGCOR_2:def 10 :
theorem
:: deftheorem Def11 defines vector_sub_prg PRGCOR_2:def 11 :
theorem