let n be Nat; :: thesis: for x, y being Element of REAL n
for m being Nat st m <= n holds
(x - y) | m = (x | m) - (y | m)
let x, y be Element of REAL n; :: thesis: for m being Nat st m <= n holds
(x - y) | m = (x | m) - (y | m)
let m be Nat; :: thesis: ( m <= n implies (x - y) | m = (x | m) - (y | m) )
assume A1: m <= n ; :: thesis: (x - y) | m = (x | m) - (y | m)
len x = n by CARD_1:def 7;
then A2: len (x | m) = m by A1, FINSEQ_1:59;
len y = n by CARD_1:def 7;
then A3: len (y | m) = m by A1, FINSEQ_1:59;
len (x - y) = n by CARD_1:def 7;
then len ((x - y) | m) = m by A1, FINSEQ_1:59;
then A5: dom ((x - y) | m) = Seg m by FINSEQ_1:def 3;
A6: dom ((x | m) - (y | m)) = (dom (x | m)) /\ (dom (y | m)) by VALUED_1:12
.= (Seg m) /\ (dom (y | m)) by FINSEQ_1:def 3, A2
.= (Seg m) /\ (Seg m) by FINSEQ_1:def 3, A3
.= Seg m ;
now :: thesis: for i being object st i in dom ((x - y) | m) holds
((x - y) | m) . i = ((x | m) - (y | m)) . i
let i be object ; :: thesis: ( i in dom ((x - y) | m) implies ((x - y) | m) . i = ((x | m) - (y | m)) . i )
assume A7: i in dom ((x - y) | m) ; :: thesis: ((x - y) | m) . i = ((x | m) - (y | m)) . i
then i in (dom (x - y)) /\ (Seg m) by RELAT_1:61;
then A8: ( i in dom (x - y) & i in Seg m ) by XBOOLE_0:def 4;
hence ((x - y) | m) . i = (x - y) . i by FUNCT_1:49
.= (x . i) - (y . i) by A8, VALUED_1:13
.= ((x | m) . i) - (y . i) by A8, FUNCT_1:49
.= ((x | m) . i) - ((y | m) . i) by A8, FUNCT_1:49
.= ((x | m) - (y | m)) . i by A5, A6, A7, VALUED_1:13 ;
:: thesis: verum
end;
hence (x - y) | m = (x | m) - (y | m) by A5, A6, FUNCT_1:2; :: thesis: verum