let S, T be non empty RelStr ; :: thesis: for s being Element of
for t being Element of holds (uparrow [s,t]) ` = [:((uparrow s) ` ),the carrier of T:] \/ [:the carrier of S,((uparrow t) ` ):]
let s be Element of ; :: thesis: for t being Element of holds (uparrow [s,t]) ` = [:((uparrow s) ` ),the carrier of T:] \/ [:the carrier of S,((uparrow t) ` ):]
let t be Element of ; :: thesis: (uparrow [s,t]) ` = [:((uparrow s) ` ),the carrier of T:] \/ [:the carrier of S,((uparrow t) ` ):]
thus (uparrow [s,t]) ` = [:the carrier of S,the carrier of T:] \ (uparrow [s,t]) by YELLOW_3:def 2
.= [:the carrier of S,the carrier of T:] \ [:(uparrow s),(uparrow t):] by YELLOW10:40
.= [:((uparrow s) ` ),the carrier of T:] \/ [:the carrier of S,((uparrow t) ` ):] by ZFMISC_1:126 ; :: thesis: verum