begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem PRGCOR_2:def 1 :
canceled;
:: deftheorem PRGCOR_2:def 2 :
canceled;
:: deftheorem PRGCOR_2:def 3 :
canceled;
:: deftheorem PRGCOR_2:def 4 :
canceled;
:: 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